proposition: Lemma applyIzero : forall (IS : IntegrationSpace) (x : X (ElemFunc IS)) (xD : Domain (Izero IS) x), partialApply (Izero IS) x xD == 0.
proof: Proof. intros. unfold Izero. rewrite applyXscale, CRmult_0_l. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions