proposition: Lemma IExtensional : forall {IS : IntegrationSpace} (f g : PartialFunction (X (ElemFunc IS))) (fL : L (ElemFunc IS) f) (gL : L (ElemFunc IS) g), (forall (x : X (ElemFunc IS)) (xF : Domain f x) (y : Domain g x), partialApply f x xF == partialApply g x y) -> I IS f fL == I IS g gL.
proof: Proof. split. + apply INonDecreasing. intros. rewrite (H x y xF). apply CRle_refl. + apply INonDecreasing. intros. rewrite (H x xF y). apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions