---

Step * of Lemma nh-comp-assoc

∀I,J,K,H:fset(ℕ). ∀f:I ⟶ J. ∀g:J ⟶ K. ∀h:K ⟶ H.  (h ⋅ g ⋅ f = h ⋅ g ⋅ f ∈ I ⟶ H)
BY
{ (Auto THEN All (RepUR ``names-hom dM nh-comp``)⋅ THEN BLemma `dma-lift-compose-assoc`  THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I,J,K,H:fset(\mBbbN{}).  \mforall{}f:I  {}\mrightarrow{}  J.  \mforall{}g:J  {}\mrightarrow{}  K.  \mforall{}h:K  {}\mrightarrow{}  H.    (h  \mcdot{}  g  \mcdot{}  f  =  h  \mcdot{}  g  \mcdot{}  f)


By

---

Latex:
(Auto  THEN  All  (RepUR  ``names-hom  dM  nh-comp``)\mcdot{}  THEN  BLemma  `dma-lift-compose-assoc`    THEN  Auto)

---

Home Index