proposition: Lemma ApplyProdLFuncApp : forall {I J : IntegrationSpace} (l k : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyL : Domain (ProdLFunc l) (x,y)) (xyK : Domain (ProdLFunc k) (x,y)) (xyDS : Domain (ProdLFunc (l ++ k)) (x,y)), partialApply (ProdLFunc (l ++ k)) (x, y) xyDS == partialApply (ProdLFunc l) (x,y) xyL + partialApply (ProdLFunc k) (x,y) xyK.
proof: Proof. induction l as [|a l]. - intros. simpl (partialApply (ProdLFunc nil) (x, y) xyL). rewrite CRplus_0_l. apply DomainProp. - intros. simpl. destruct xyDS, d, xyL, d2. simpl. rewrite CRplus_assoc. apply CRplus_morph. + destruct d. destruct d2. 2: contradiction. destruct d1. destruct d4. 2: contradiction. reflexivity. destruct d4. contradiction. reflexivity. rewrite CRmult_0_r, CRmult_0_l. destruct d2. contradiction. rewrite CRmult_0_r, CRmult_0_l. reflexivity. + apply IHl. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile