proposition: Lemma IntegralRestrict : forall {IS : IntegrationSpace} (f g : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (restrict : PartialRestriction f g), Integral (IntegrableFunctionExtensional f g restrict fInt) = Integral fInt.
proof: Proof. intros. destruct fInt, restrict, p; simpl. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase