Step 
*
 of Lemma 
name-morph-ap
∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[x:nameset(I)].  (f x ∈ extd-nameset(J))
BY
 
{ Auto }
 
Latex: 
Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].  \mforall{}[x:nameset(I)].    (f  x  \mmember{}  extd-nameset(J))
 By 
Latex:
Auto
Home
Index