---

Step * of Lemma trans-horizontal-comp_wf

∀[C,D,E:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[J,K:Functor(D;E)]. ∀[tFG:nat-trans(C;D;F;G)]. ∀[tJK:nat-trans(D;E;J;K)].
  (trans-horizontal-comp(E;F;G;J;K;tFG;tJK) ∈ nat-trans(C;E;functor-comp(F;J);functor-comp(G;K)))
BY
{ (ProveWfLemma THEN RepUR ``functor-comp`` 0 THEN RW CatNormC 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C,D,E:SmallCategory].  \mforall{}[F,G:Functor(C;D)].  \mforall{}[J,K:Functor(D;E)].  \mforall{}[tFG:nat-trans(C;D;F;G)].
\mforall{}[tJK:nat-trans(D;E;J;K)].
    (trans-horizontal-comp(E;F;G;J;K;tFG;tJK)  \mmember{}  nat-trans(C;E;functor-comp(F;J);functor-comp(G;K)))


By

---

Latex:
(ProveWfLemma  THEN  RepUR  ``functor-comp``  0  THEN  RW  CatNormC  0  THEN  Auto)

---

Home Index