proposition: Lemma axioms_extensionality : forall f g, axioms f -> axioms g -> source f = source g -> target f = target g -> (forall u, mor (source f) u-> fmor f u = fmor g u) -> f = g.
proof: Proof. ir. wr (create_recovers H). wr (create_recovers H0). wr H1. wr H2. uf create. uf Umorphism.create. ap uneq. ap Function.create_extensionality. tv. ir. ap H3. change (is_mor (source f) x) in H4. app is_mor_mor. uh H; ee. am. Qed.
imports: Arith category