---

Step * of Lemma uext-ap-name

∀[I,J:Cname List]. ∀[g:name-morph(I;J)]. ∀[x:nameset(I)].  ((uext(g) x) = (g x) ∈ extd-nameset(J))
BY
{ (Auto THEN Unfold `uext` 0 THEN Reduce 0 THEN RWO  "isname-name" 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `uext`  0  THEN  Reduce  0  THEN  RWO    "isname-name"  0  THEN  Reduce  0  THEN  Auto)

---

Home Index