---

Step * 3 1 of Lemma topfuneq-equiv


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. ∀x:|X|. topeq(Y;b x;c x)
9. x : |X|
10. topeq(Y;b x;c x)
⊢ topeq(Y;a x;c x)
BY
{ (D -4 With ⌜x⌝  THENA Auto) }

1
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. ∀x:|X|. topeq(Y;b x;c x)
8. x : |X|
9. topeq(Y;b x;c x)
10. topeq(Y;a x;b x)
⊢ topeq(Y;a x;c x)

---

Latex:

---

Latex:

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.  \mforall{}x:|X|.  topeq(Y;b  x;c  x)
9.  x  :  |X|
10.  topeq(Y;b  x;c  x)
\mvdash{}  topeq(Y;a  x;c  x)


By

---

Latex:
(D  -4  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)

---

Home Index