the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.]
by TOPMETR:18;
then reconsider j = 1, k = - 1 as Point of (Closed-Interval-TSpace ((- 1),1)) by XXREAL_1:1;
reconsider z = 0 , o = 1 as Point of I[01] by BORSUK_1:40, XXREAL_1:1;
let T be non empty TopSpace; ( T is T_4 implies T is Tychonoff )
assume A11:
T is T_4
; T is Tychonoff
let A be closed Subset of T; TOPGEN_5:def 4 for a being Point of T st a in A ` holds
ex f being continuous Function of T,I[01] st
( f . a = 0 & f .: A c= {1} )
let a be Point of T; ( a in A ` implies ex f being continuous Function of T,I[01] st
( f . a = 0 & f .: A c= {1} ) )
per cases
( A is empty or not A is empty )
;
suppose
not
A is
empty
;
( a in A ` implies ex f being continuous Function of T,I[01] st
( f . a = 0 & f .: A c= {1} ) )then reconsider aa =
{a},
A9 =
A as non
empty closed Subset of
T by A11, URYSOHN1:19;
reconsider B =
A9 \/ aa as
closed Subset of
T ;
set h =
((T | A9) --> j) +* ((T | aa) --> k);
A14:
(T | aa) --> k = aa --> k
by PRE_TOPC:8;
A15:
(A9 --> 1) .: A c= {1}
by FUNCOP_1:81;
A16:
a in aa
by TARSKI:def 1;
then A17:
a in B
by XBOOLE_0:def 3;
assume
a in A `
;
ex f being continuous Function of T,I[01] st
( f . a = 0 & f .: A c= {1} )then A18:
not
a in A
by XBOOLE_0:def 5;
then
A9 misses aa
by ZFMISC_1:50;
then reconsider h =
((T | A9) --> j) +* ((T | aa) --> k) as
continuous Function of
(T | B),
(Closed-Interval-TSpace ((- 1),1)) by Th11;
consider g being
continuous Function of
T,
(Closed-Interval-TSpace ((- 1),1)) such that A19:
g | B = h
by A11, TIETZE:23;
consider p being
Function of
I[01],
(Closed-Interval-TSpace ((- 1),1)) such that A20:
p is
being_homeomorphism
and
for
r being
Real st
r in [.0,1.] holds
p . r = (2 * r) - 1
and A21:
p . 0 = - 1
and A22:
p . 1
= 1
by JGRAPH_5:39;
reconsider p9 =
p /" as
continuous Function of
(Closed-Interval-TSpace ((- 1),1)),
I[01] by A20, TOPS_2:def 5;
A23:
p9 = p "
by A20, TOPS_2:def 4;
then A24:
p9 . k = z
by A20, A21, FUNCT_2:26;
A25:
the
carrier of
(T | aa) = aa
by PRE_TOPC:8;
then
dom ((T | aa) --> k) = aa
;
then A26:
h . a =
((T | aa) --> k) . a
by A16, FUNCT_4:13
.=
- 1
by A25, A16, FUNCOP_1:7
;
reconsider f =
p9 * g as
continuous Function of
T,
I[01] ;
A27:
f .: A =
p9 .: (g .: A)
by RELAT_1:126
.=
p9 .: (h .: A)
by A19, RELAT_1:129, XBOOLE_1:7
;
(T | A9) --> j = A9 --> 1
by PRE_TOPC:8;
then
h .: A c= {1}
by A14, A15, A18, BOOLMARK:3, ZFMISC_1:50;
then A28:
f .: A c= Im (
p9,1)
by A27, RELAT_1:123;
take
f
;
( f . a = 0 & f .: A c= {1} )thus f . a =
p9 . (g . a)
by FUNCT_2:15
.=
0
by A26, A17, A19, A24, FUNCT_1:49
;
f .: A c= {1}
p9 . j = o
by A20, A22, A23, FUNCT_2:26;
hence
f .: A c= {1}
by A28, SETWISEO:8;
verum end;