proposition: Lemma ProdIntegrableSimplifyEq : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyH : Domain (ProdLFunc hn) (x,y)) (xyS : Domain (ProdLFunc (ProdIntegrableSimplify hn)) (x,y)), partialApply _ _ xyH == partialApply _ _ xyS.
proof: Proof. intros. rewrite (ProdIntegrableSimplifyApply hn x y xyH). apply ApplyIntersectFactor. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile