proposition: Lemma IntegralRepresentationInvariant : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fnInt gnInt : IntegrableFunction f), Integral fnInt == Integral gnInt.
proof: Proof. intros. assert (forall (x : X (ElemFunc IS)) (xD : Domain (Xplus f (Xscale (-(1)) f)) x), partialApply (Xplus f (Xscale (-(1)) f)) x xD == 0). { intros. destruct xD. rewrite (applyXplus f (Xscale (- (1)) f)), applyXscale. rewrite (DomainProp f x d d0), <- CRopp_mult_distr_l, CRmult_1_l. apply CRplus_opp_r. } pose proof (IntegralRepresentationInvariantZero (Xminus f f) (IntegrableMinus fnInt gnInt) H) as invZero. rewrite IntegralMinus in invZero. apply (CRplus_eq_reg_l (-Integral gnInt)). rewrite CRplus_opp_l, CRplus_comm. exact invZero. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase