---

Step * of Lemma topfuneq-equiv-ext

∀X,Y:Space.  EquivRel(topfun(X;Y);f,g.topfuneq(X;Y;f;g))
BY
{ Extract of Obid: topfuneq-equiv
  normalizes to:
  
  λX,Y. tfunequiv(X;Y)
  finishing with (Unfold `tfunequiv` 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  topfuneq-equiv
normalizes  to:

\mlambda{}X,Y.  tfunequiv(X;Y)
finishing  with  (Unfold  `tfunequiv`  0  THEN  Auto)

---

Home Index