proposition: Lemma IntegralExtensionalAE : forall {IS : IntegrationSpace} (f g : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (gInt : IntegrableFunction g), almost_everywhere (fun x : X (ElemFunc IS) => forall (dF : Domain f x) (dG : Domain g x), partialApply _ _ dF == partialApply _ _ dG) -> Integral fInt == Integral gInt.
proof: Proof. intros. split. - apply IntegralNonDecreasingAE. destruct X as [h [hInt p]]. exists h. split. exact hInt. intros x dfull dG dF. rewrite (p x dfull dF dG). apply CRle_refl. - apply IntegralNonDecreasingAE. destruct X as [h [hInt p]]. exists h. split. exact hInt. intros x dfull dF dG. rewrite (p x dfull dF dG). apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions