proposition: Lemma PrependSeqL : forall (E : FunctionRieszSpace) (f : PartialFunction (X E)) (un : nat -> PartialFunction (X E)), L E f -> (forall n:nat, L E (un n)) -> forall n:nat, L E (PrependSeq f un n).
proof: Proof. intros E f un H H0 n. unfold PrependSeq. destruct n. exact H. apply H0. Defined.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions