---

Step * of Lemma is-mfun-compose

No Annotations
∀[X,Y,Z:Type]. ∀[d:metric(X)]. ∀[d':metric(Y)]. ∀[d'':metric(Z)]. ∀[f:X ⟶ Y]. ∀[g:Y ⟶ Z].
  (g  o f:FUN(X;Z)) supposing (g:FUN(Y;Z) and f:FUN(X;Y))
BY
{ (Auto
   THEN RepeatFor 2 (ParallelOp -2)
   THEN RepeatFor 2 (ParallelLast)
   THEN UnfoldTopAb 10
   THEN FHyp 10 [-1]
   THEN Auto
   THEN RepUR ``compose so_apply`` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y,Z:Type].  \mforall{}[d:metric(X)].  \mforall{}[d':metric(Y)].  \mforall{}[d'':metric(Z)].  \mforall{}[f:X  {}\mrightarrow{}  Y].  \mforall{}[g:Y  {}\mrightarrow{}  Z].
    (g    o  f:FUN(X;Z))  supposing  (g:FUN(Y;Z)  and  f:FUN(X;Y))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (ParallelOp  -2)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  UnfoldTopAb  10
  THEN  FHyp  10  [-1]
  THEN  Auto
  THEN  RepUR  ``compose  so\_apply``  0
  THEN  Auto)

---

Home Index