---

Step * of Lemma tfunequiv_wf

∀X,Y:Space.  (tfunequiv(X;Y) ∈ EquivRel(topfun(X;Y);f,g.topfuneq(X;Y;f;g)))
BY
{ (Auto THEN (Subst' tfunequiv(X;Y) ~ TERMOF{topfuneq-equiv-ext:o, \\v:l, i:l} X Y 0 THENA Computation) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}X,Y:Space.    (tfunequiv(X;Y)  \mmember{}  EquivRel(topfun(X;Y);f,g.topfuneq(X;Y;f;g)))


By

---

Latex:
(Auto
  THEN  (Subst'  tfunequiv(X;Y)  \msim{}  TERMOF\{topfuneq-equiv-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  X  Y  0  THENA  Computation)
  THEN  Auto)

---

Home Index