proposition: Lemma IntegralExtensional : forall {IS : IntegrationSpace} (f g : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (gInt : IntegrableFunction g), (forall (x : X (ElemFunc IS)) (xdf : Domain f x) (xdg : Domain g x), partialApply f x xdf == partialApply g x xdg) -> Integral fInt == Integral gInt.
proof: Proof. split. - apply IntegralNonDecreasing. intros x xdf xdg. rewrite (H x xdg xdf). apply CRle_refl. - apply IntegralNonDecreasing. intros x xdf xdg. rewrite (H x xdf xdg). apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase