---

Step * of Lemma csm-universe-comp-op

No Annotations
∀[E,s:Top].  ((compOp(E))s ~ compOp((E)s))
BY
{ ((Auto THEN RepUR ``universe-comp-op csm-composition`` 0) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[E,s:Top].    ((compOp(E))s  \msim{}  compOp((E)s))


By

---

Latex:
((Auto  THEN  RepUR  ``universe-comp-op  csm-composition``  0)  THEN  Auto)

---

Home Index