proposition: Lemma restr_to_domain : forall f g, Function.axioms f -> Function.axioms g -> sub f g -> restr g (domain f) = f.
proof: Proof. ir. sy. ap function_sub_eq. am. ap restr_axioms. am. uhg; ir. uf restr; ap Z_inc. ap H1; am. uf domain. rw Image.inc_rw. sh x; ee; try am; try tv. rw restr_domain. uhg; ir. cp (intersection2_second H2). am. am. Qed.
imports: set_theory