---

Step * 3 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. topfuneq(X;Y;b;c)
⊢ topfuneq(X;Y;a;c)
BY
{ RepeatFor 2 (ParallelLast) }

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. 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)

---

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.  topfuneq(X;Y;b;c)
\mvdash{}  topfuneq(X;Y;a;c)


By

---

Latex:
RepeatFor  2  (ParallelLast)

---

Home Index