---

Step * of Lemma es-local-embedding-compose

∀[Info:Type]. ∀[eo1,eo2,eo3:EO+(Info)]. ∀[f:E ─→ E]. ∀[g:E ─→ E].
  (es-local-embedding(Info;eo1;eo2;f) ⇒ es-local-embedding(Info;eo2;eo3;g) ⇒ es-local-embedding(Info;eo1;eo3;g o f))
BY
{ (Auto
   THEN All (RepUR ``es-local-embedding``)
   THEN Auto
   THEN (InstHyp [⌈e⌉] 7⋅ THENA Auto)
   THEN InstHyp [⌈f e⌉] 8⋅
   THEN Auto) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[eo1,eo2,eo3:EO+(Info)].  \mforall{}[f:E  {}\mrightarrow{}  E].  \mforall{}[g:E  {}\mrightarrow{}  E].
    (es-local-embedding(Info;eo1;eo2;f)
    {}\mRightarrow{}  es-local-embedding(Info;eo2;eo3;g)
    {}\mRightarrow{}  es-local-embedding(Info;eo1;eo3;g  o  f))


By

(Auto
  THEN  All  (RepUR  ``es-local-embedding``)
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  7\mcdot{}  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}f  e\mkleeneclose{}]  8\mcdot{}
  THEN  Auto)

---

Home Index