fact: Definition ProdLFunc {I J : IntegrationSpace} : list (@ProdIntegrable I J) -> PartialFunction (prod (X (ElemFunc I)) (X (ElemFunc J))) := fun l => XsumList (map ProdIntegrableFunc l).
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile