---

Step * 1 1 of Lemma poset-functor-comp


1. I : Cname List
2. J : Cname List
3. K : Cname List
4. f : name-morph(I;J)
5. g : name-morph(J;K)
6. x : name-morph(K;[])
⊢ ((f o g) o x) = (f o (g o x)) ∈ name-morph(I;[])
BY
{ Auto }

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  Cname  List
3.  K  :  Cname  List
4.  f  :  name-morph(I;J)
5.  g  :  name-morph(J;K)
6.  x  :  name-morph(K;[])
\mvdash{}  ((f  o  g)  o  x)  =  (f  o  (g  o  x))


By

---

Latex:
Auto

---

Home Index