proposition: Lemma LsumStable : forall {Elem : FunctionRieszSpace} (fn : nat -> PartialFunction (X Elem)) (fnL : forall n:nat, L Elem (fn n)), forall n:nat, L Elem (Xsum fn n).
proof: Proof. induction n. simpl. apply fnL. simpl. apply (LplusStable Elem). exact IHn. apply fnL. Defined.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions