---

Step * of Lemma cat_comp_assoc

∀[C:SmallCategory]
  ∀x,y,z,w:cat-ob(C). ∀f:cat-arrow(C) x y. ∀g:cat-arrow(C) y z. ∀h:cat-arrow(C) z w.
    (h o g o f = h o g o f ∈ (cat-arrow(C) x w))
BY
{ ((Unfold `cat_comp` 0 THEN Auto) THEN BLemma `cat-comp-assoc`) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory]
    \mforall{}x,y,z,w:cat-ob(C).  \mforall{}f:cat-arrow(C)  x  y.  \mforall{}g:cat-arrow(C)  y  z.  \mforall{}h:cat-arrow(C)  z  w.
        (h  o  g  o  f  =  h  o  g  o  f)


By

---

Latex:
((Unfold  `cat\_comp`  0  THEN  Auto)  THEN  BLemma  `cat-comp-assoc`)

---

Home Index