proposition: Lemma ProdIntegrableFuncIntegrable : forall {I J : IntegrationSpace } (a : ProdIntegrable), IntegrableFunction (IntegralFst (ProdIntegrableFunc a) (@ProdIntegrableFuncIntegrableAE I J a)).
proof: Proof. intros. apply (IntegrableFunctionExtensional (Xscale (prodint_factor a * CRcast (Integral (prodint_gint a))) (CharacFunc (prodint_f a)))). 2: apply IntegrableScale, a. split. intros x xD. exact xD. intros. simpl in xD, xG. unfold ProdIntegrableFuncIntegrableAE, IntegralFst, partialApply; rewrite IntegralRestrict. rewrite (@IntegralScale (IntegrationSpaceCast J)), IntegralRestrict, IntegralFunctionCast. simpl. destruct xD. destruct xG. 2: contradiction. do 2 rewrite CRmult_1_r. rewrite CRmult_comm. reflexivity. destruct xG. contradiction. do 3 rewrite CRmult_0_r. reflexivity. Defined.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile