---

Step * 1 of Lemma name-comp-assoc


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))
BY
{ Thin (-1) }

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))
⊢ ((f o g) o h) = (f o (g o h)) ∈ (nameset(I) ⟶ extd-nameset(H))

---

Latex:

---

Latex:

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)
9.  \mforall{}i,j:nameset(I).
          ((\muparrow{}isname(((f  o  g)  o  h)  i))
          {}\mRightarrow{}  (\muparrow{}isname(((f  o  g)  o  h)  j))
          {}\mRightarrow{}  ((((f  o  g)  o  h)  i)  =  (((f  o  g)  o  h)  j))
          {}\mRightarrow{}  (i  =  j))
\mvdash{}  ((f  o  g)  o  h)  =  (f  o  (g  o  h))


By

---

Latex:
Thin  (-1)

---

Home Index