---

Step * of Lemma name-morph-ext

∀[I,J:Cname List]. ∀[f,g:name-morph(I;J)].
  f = g ∈ name-morph(I;J) supposing ∀x:nameset(I). ((f x) = (g x) ∈ extd-nameset(J))
BY
{ (Auto THEN BLemma `name-morphs-equal` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f,g:name-morph(I;J)].    f  =  g  supposing  \mforall{}x:nameset(I).  ((f  x)  =  (g  x))


By

---

Latex:
(Auto  THEN  BLemma  `name-morphs-equal`  THEN  Auto)

---

Home Index