---

Step * of Lemma name-comp-id-right

∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  ((f o 1) = f ∈ name-morph(I;J))
BY
{ (Auto THEN D -1 THEN Symmetry THEN (MemTypeCD THENA Auto)) }

1
1. I : Cname List
2. J : Cname List
3. f : nameset(I) ⟶ extd-nameset(J)
4. ∀i,j:nameset(I).  ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))
⊢ f = (f o 1) ∈ (nameset(I) ⟶ extd-nameset(J))

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].    ((f  o  1)  =  f)


By

---

Latex:
(Auto  THEN  D  -1  THEN  Symmetry  THEN  (MemTypeCD  THENA  Auto))

---

Home Index