proposition: Lemma CSUCIntegrableProper : forall {R : ConstructiveReals} (fn : nat -> PartialFunction (CRcarrier R)) (x y : CRcarrier R) (xD : Domain (XinfiniteSumAbs fn) x) (yD : Domain (XinfiniteSumAbs fn) y), (forall n : nat, Is_CSUC_func (fn n)) -> x == y -> partialApply _ x xD == partialApply _ y yD.
proof: Proof. intros. simpl. destruct xD, yD. simpl in c, c0. apply series_cv_abs_eq. apply (series_cv_eq (fun n : nat => partialApply (fn n) x0 (x1 n))). 2: apply series_cv_abs_cv. intro n. specialize (H n). destruct H, CSUC_adapt0. pose proof (UniformContProper _ _ u x0 y0 H0). unfold TotalizeFunc in H. transitivity (partialApply (fn n) x0 (CSUC_fullDomain0 x0)). apply DomainProp. rewrite H. apply DomainProp. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets