proposition: Lemma SumProdIntFIntegrable : forall { I J : IntegrationSpace } (l : list (@ProdIntegrable I J)), IntegrableFunction (XsumList (map (fun x : ProdIntegrable => CharacFunc (prodint_f x)) l)).
proof: Proof. induction l. - simpl. apply IntegrableZero. - simpl. apply IntegrablePlus. apply a. apply IHl. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile