---

Step * of Lemma functor-comp_wf

∀[A,B,C:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;C)].  (functor-comp(F;G) ∈ Functor(A;C))
BY
{ (ProveWfLemma THEN NormCatEq THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:SmallCategory].  \mforall{}[F:Functor(A;B)].  \mforall{}[G:Functor(B;C)].    (functor-comp(F;G)  \mmember{}  Functor(A;C))


By

---

Latex:
(ProveWfLemma  THEN  NormCatEq  THEN  Auto)

---

Home Index