---

Step * of Lemma topfuneq-equiv

∀X,Y:Space.  EquivRel(topfun(X;Y);f,g.topfuneq(X;Y;f;g))
BY
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
1. X : Space
2. Y : Space
3. a : topfun(X;Y)
⊢ topfuneq(X;Y;a;a)

2
1. X : Space
2. Y : Space
3. a : topfun(X;Y)
4. b : topfun(X;Y)
5. topfuneq(X;Y;a;b)
⊢ topfuneq(X;Y;b;a)

3
1. X : Space
2. Y : Space
3. Sym(topfun(X;Y);f,g.topfuneq(X;Y;f;g))
4. a : topfun(X;Y)
5. b : topfun(X;Y)
6. c : topfun(X;Y)
7. topfuneq(X;Y;a;b)
8. topfuneq(X;Y;b;c)
⊢ topfuneq(X;Y;a;c)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index