---

Step * of Lemma name-comp-assoc

∀[I,J,K,H:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:name-morph(J;K)]. ∀[h:name-morph(K;H)].
  (((f o g) o h) = (f o (g o h)) ∈ name-morph(I;H))
BY
{ (Auto
   THEN (Assert ((f o g) o h) ∈ name-morph(I;H) BY
               Auto)
   THEN (MemTypeHD (-1) THENA Auto)
   THEN MemTypeCD
   THEN Auto) }

1
1. I : Cname List
2. J : Cname List
3. K : Cname List
4. H : Cname List
5. f : name-morph(I;J)
6. g : name-morph(J;K)
7. h : name-morph(K;H)
8. ((f o g) o h) = ((f o g) o h) ∈ (nameset(I) ⟶ extd-nameset(H))
9. ∀i,j:nameset(I).
     ((↑isname(((f o g) o h) i))
     ⇒ (↑isname(((f o g) o h) j))
     ⇒ ((((f o g) o h) i) = (((f o g) o h) j) ∈ extd-nameset(H))
     ⇒ (i = j ∈ nameset(I)))
⊢ ((f o g) o h) = (f o (g o h)) ∈ (nameset(I) ⟶ extd-nameset(H))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  ((f  o  g)  o  h)  \mmember{}  name-morph(I;H)  BY
                          Auto)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index