proposition: Lemma ApplyMapCoef : forall {I J : IntegrationSpace} (a : CRcarrier (RealT (ElemFunc I))) (l : list ProdIntegrable) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyDS : Domain (ProdLFunc (map (ProdIntegrableMapCoef (fun x0 : CRcarrier _ => a * x0)) l)) (x,y)), partialApply _ (x, y) xyDS == a * partialApply (ProdLFunc l) (x, y) (DomainProdLFuncMap l x y (fun x0 : CRcarrier _ => a * x0) xyDS).
proof: Proof. induction l. - intros. simpl. rewrite CRmult_0_r. reflexivity. - intros. simpl. destruct xyDS. rewrite IHl. destruct (DomainProdLFuncMap (a0 :: l) x y (fun x0 : CRcarrier _ => a * x0) (d, d0)). rewrite CRmult_assoc, CRmult_assoc, <- CRmult_plus_distr_l. apply CRmult_morph. reflexivity. apply CRplus_morph. 2: apply DomainProp. destruct d, d1. simpl. destruct d. destruct d1. 2: contradiction. destruct d3. destruct d4. 2: contradiction. rewrite CRmult_assoc. reflexivity. destruct d4. contradiction. rewrite CRmult_assoc. reflexivity. rewrite CRmult_0_l. destruct d1. contradiction. rewrite CRmult_0_r, CRmult_0_l. reflexivity. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile