proposition: Lemma IhomogeneousCast : forall (IS : IntegrationSpace) {R : ConstructiveReals} (a : CRcarrier (RealT (FunctionRieszSpaceCast (ElemFunc IS)))) (f : PartialFunction (X (FunctionRieszSpaceCast (ElemFunc IS)))) (fL : L (FunctionRieszSpaceCast (ElemFunc IS)) f), CRcast (I IS (PartialFunctionCast (Xscale a f)) (LscaleStable (@FunctionRieszSpaceCast R (ElemFunc IS)) a f fL)) == a * CRcast (I IS (PartialFunctionCast f) fL).
proof: Proof. intros. unfold CRcast. rewrite (CRmorph_proper _ (I IS (PartialFunctionCast (Xscale a f)) (LscaleStable (FunctionRieszSpaceCast (ElemFunc IS)) a f fL)) (CRcast a * I IS (PartialFunctionCast f) fL)). rewrite CRmorph_mult. apply CRmult_morph. unfold CRcast. simpl in a. transitivity (CRmorph (CRmorph_compose (@SlowConstructiveRealsMorphism (RealT (FunctionRieszSpaceCast (ElemFunc IS))) (RealT (ElemFunc IS))) (@SlowConstructiveRealsMorphism (RealT (ElemFunc IS)) R) ) a). unfold CRmorph_compose, CRmorph. reflexivity. apply Endomorph_id. reflexivity. rewrite <- (Ihomogeneous IS). apply IExtensional. intros. simpl. unfold CRcast. rewrite <- CRmorph_mult. apply CRmorph_proper. apply CRmult_morph. reflexivity. apply DomainProp. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets