---

Step * of Lemma compose-mfun

∀[X,Y,Z:Type]. ∀[dX:metric(X)]. ∀[dY:metric(Y)]. ∀[dZ:metric(Z)]. ∀[f:FUN(X ⟶ Y)]. ∀[g:FUN(Y ⟶ Z)].
  (g o f ∈ FUN(X ⟶ Z))
BY
{ (Unfold `mfun` 0
   THEN Auto
   THEN DSetVars
   THEN MemTypeCD
   THEN Auto
   THEN All (RepUR ``is-mfun so_apply``)
   THEN ParallelOp -3
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X,Y,Z:Type].  \mforall{}[dX:metric(X)].  \mforall{}[dY:metric(Y)].  \mforall{}[dZ:metric(Z)].  \mforall{}[f:FUN(X  {}\mrightarrow{}  Y)].
\mforall{}[g:FUN(Y  {}\mrightarrow{}  Z)].
    (g  o  f  \mmember{}  FUN(X  {}\mrightarrow{}  Z))


By

---

Latex:
(Unfold  `mfun`  0
  THEN  Auto
  THEN  DSetVars
  THEN  MemTypeCD
  THEN  Auto
  THEN  All  (RepUR  ``is-mfun  so\_apply``)
  THEN  ParallelOp  -3
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto)

---

Home Index