proposition: Lemma IadditiveCast : forall (IS : IntegrationSpace) {R : ConstructiveReals} (f g : PartialFunction (X (FunctionRieszSpaceCast (ElemFunc IS)))) (fL : L (FunctionRieszSpaceCast (ElemFunc IS)) f) (gL : L (FunctionRieszSpaceCast (ElemFunc IS)) g), CRcast (I IS (PartialFunctionCast (Xplus f g)) (LplusStable (@FunctionRieszSpaceCast R (ElemFunc IS)) f g fL gL)) == CRcast (I IS (PartialFunctionCast f) fL) + @CRcast (RealT (ElemFunc IS)) R (I IS (PartialFunctionCast g) gL).
proof: Proof. intros. unfold CRcast. rewrite <- CRmorph_plus. apply CRmorph_proper. rewrite <- (Iadditive IS). apply IExtensional. intros. simpl. destruct xF, y. unfold CRcast. rewrite <- CRmorph_plus. apply CRmorph_proper. apply CRplus_morph; apply DomainProp. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets