proposition: Lemma LElemProductIntegralFstIntegrable : forall { I J : IntegrationSpace } (l : list (@ProdIntegrable I J)), IntegrableFunction (IntegralFst (ProdLFunc l) (LElemProductIntegrableAE l)).
proof: Proof. induction l. - unfold IntegralFst; destruct (LElemProductIntegrableAE nil) as [f p], p. apply (IntegrableFunctionExtensional (Xscale 0 f)). split. intros x H; exact H. intros; unfold Domain in xG. simpl. rewrite CRmult_0_l. rewrite (IntegralExtensional _ _ (i0 x xG) IntegrableZero). symmetry. apply (@IntegralZeroIsZero (IntegrationSpaceCast J)). intros. reflexivity. apply IntegrableScale, i. - apply (IntegrableFunctionExtensional (Xplus (IntegralFst _ (ProdIntegrableFuncIntegrableAE a)) (IntegralFst (ProdLFunc l) (LElemProductIntegrableAE l)))). split. + unfold IntegralFst. unfold LElemProductIntegrableAE. intros x [d d0]; unfold Domain in d0; simpl in d; split. exact d. exact d0. + intros. unfold IntegralFst. unfold LElemProductIntegrableAE, Xplus, XbinOp, XbinOpXY, partialApply. destruct xD. unfold ProdIntegrableFuncIntegrableAE; rewrite IntegralRestrict. rewrite <- (@IntegralPlus (IntegrationSpaceCast J) _ _ _ (LElemProductIntegrableAEspec l x d0)); apply (@IntegralExtensional (IntegrationSpaceCast J)). intros. destruct xdf, xdg. unfold ProdLFunc. apply CRplus_morph. apply CRmult_morph. apply CRmult_morph. reflexivity. apply DomainProp. apply DomainProp. simpl. apply DomainProp. + apply IntegrablePlus. 2: exact IHl. clear IHl. apply ProdIntegrableFuncIntegrable. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile