proposition: Lemma trans_map_axioms : forall x y f, Transformation.axioms x y f = Map.axioms x y (Function.create x f).
proof: Proof. ir. ap iff_eq; ir. uhg; ee. ap create_axioms. rw create_domain. tv. uhg; ir. rwi create_range H0. rwi Image.inc_rw H0. nin H0. ee. wr H1. uh H; ee. ap H. am. uhg. ir. uh H; ee. uh H2. ap H2. rw create_range. rw Image.inc_rw. sh x0. ee; try am; try tv. Qed.
imports: set_theory