proposition: Lemma LElemFuncCastReverse : forall (E : FunctionRieszSpace) {R : ConstructiveReals} (f : PartialFunction (X E)), L E f -> L (@FunctionRieszSpaceCast R E) (PartialFunctionCast f).
proof: Proof. intros E R f fL. simpl. apply (Lext _ f). split. split. intros x xD. exact xD. intros x xD. exact xD. intros. simpl. unfold CRcast. transitivity (CRmorph (CRmorph_compose (@SlowConstructiveRealsMorphism (RealT E) R) (@SlowConstructiveRealsMorphism (RealT (FunctionRieszSpaceCast E)) (RealT E)) ) (partialApply f x xG)). rewrite Endomorph_id. apply DomainProp. reflexivity. apply fL. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets