proposition: Lemma ApplyIntersectFactor : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyH : Domain (ProdLFunc hn) (x,y)), partialApply (ProdLFunc hn) (x, y) xyH == SubsetIntersectFactor hn (ProdIntegrableSubsetLeft hn x y xyH) (ProdIntegrableSubsetRight hn x y xyH).
proof: Proof. induction hn. - reflexivity. - intros. destruct xyH. specialize (IHhn x y d0). simpl. rewrite IHhn. clear IHhn. destruct d. simpl. rewrite CRplus_comm. apply CRplus_morph. reflexivity. destruct d. destruct d1. do 2 rewrite CRmult_1_r. reflexivity. rewrite CRmult_1_r. rewrite CRmult_0_r. reflexivity. destruct d1. rewrite CRmult_0_r, CRmult_0_l. reflexivity. rewrite CRmult_0_r. reflexivity. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile