proposition: Lemma LElemProductIntegrableAE : forall { I J : IntegrationSpace } (l : list (@ProdIntegrable I J)), IntegrableFunctionAE (ProdLFunc l).
proof: Proof. intros I J l. exists (XsumList (map (fun x => CharacFunc (prodint_f x)) l)). split. - apply SumProdIntFIntegrable. - apply LElemProductIntegrableAEspec. Defined.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile