proposition: Lemma applyPackFirstSum : forall {R : ConstructiveReals} (X : Set) (fn : nat -> @PartialFunction R X) (n N : nat) (x : X) (pxDn : forall n:nat, Domain (fn n) x) (pxDnP : forall n:nat, Domain (PackFirstFunctions X fn N n) x), (CRsum (fun k => partialApply (PackFirstFunctions X fn N k) x (pxDnP k)) n == CRsum (fun k => partialApply (fn k) x (pxDn k)) (n+N)).
proof: Proof. induction n. - intros. simpl. rewrite (applyXsum _ _ _ (pxDnP O) pxDn). reflexivity. - intros. simpl. rewrite (IHn N x pxDn). clear IHn. apply CRplus_morph. reflexivity. replace (S (n + N)) with (N + S n)%nat. apply DomainProp. rewrite Nat.add_comm. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions