proposition: Lemma trans_map_bijective : forall x y f, Transformation.bijective x y f = Map.bijective x y (Function.create x f).
proof: Proof. ir. ap iff_eq; ir. uhg; ee. wr trans_map_axioms; uh H; ee; am. wr trans_map_surjective; uh H; ee; am. wr trans_map_injective; uh H; ee; am. uhg; ee. rw trans_map_axioms; uh H; ee; am. rw trans_map_surjective; uh H; ee; am. rw trans_map_injective; uh H; ee; am. Qed.
imports: set_theory