proposition: Lemma represApply : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegralRepresentation) (isFInt : PartialRestriction (XinfiniteSumAbs (IntFn fInt)) f) (x : X (ElemFunc IS)) (xS : Domain (XinfiniteSumAbs (IntFn fInt)) x) (y : Domain f x), series_cv (fun n : nat => partialApply (IntFn fInt n) x (domainInfiniteSumAbsIncReverse (IntFn fInt) x xS n)) (partialApply f x y).
proof: Proof. intros. destruct isFInt as [i appX]. specialize (appX x xS y). apply (CR_cv_proper _ (partialApply (XinfiniteSumAbs (IntFn fInt)) x xS)). 2: exact appX. clear appX. simpl. destruct xS; simpl. destruct (series_cv_abs (fun n : nat => partialApply (IntFn fInt n) x (x0 n))). exact s. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase