proposition: Lemma PackFirstFunctionsL : forall (IS : IntegrationSpace) (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnL : forall n:nat, L (ElemFunc IS) (fn n)) (n p : nat), L (ElemFunc IS) (PackFirstFunctions (X (ElemFunc IS)) fn n p).
proof: Proof. intros. unfold PackFirstFunctions. destruct p. - apply LsumStable. apply fnL. - apply fnL. Defined.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions