proposition: Lemma restr_ev : forall f u x, Function.axioms f -> sub u (domain f) -> inc x u -> V x (restr f u) = V x f.
proof: Proof. ir. util (Function.defined_lem (f:=f) (x:=x)). am. uhg. ee. am. ap H0; am. cp (restr_sub (f:=f) (x:= u)). assert (inc (pair x (V x f)) (restr f u)). uf restr; ap Z_inc; ee. am. rw pr1_pair. am. cp Function.pr2_V. assert (Function.axioms (restr f u)). ap restr_axioms; try am. cp (H5 _ _ H6 H4). rwi pr2_pair H7. rwi pr1_pair H7. sy; am. Qed.
imports: set_theory