---

Step * of Lemma name-comp-id-left

∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  ((1 o f) = 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 = (1 o f) ∈ (nameset(I) ⟶ extd-nameset(J))

---

Latex:

---

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


By

---

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

---

Home Index