the carrier of (Closed-Interval-TSpace (- 1),1) = [.(- 1),1.] by TOPMETR:25;
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:83, XXREAL_1:1;
let T be non empty TopSpace; :: thesis: ( T is T_4 implies T is Tychonoff )
assume A11: T is T_4 ; :: thesis: T is Tychonoff
let A be closed Subset of T; :: according to TOPGEN_5:def 4 :: thesis: 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; :: thesis: ( 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 A12: A is empty ; :: thesis: ( a in A ` implies ex f being continuous Function of T,I[01] st
( f . a = 0 & f .: A c= {1} ) )

set f = T --> z;
A13: (T --> z) . a = z by FUNCOP_1:13;
(T --> z) .: A = {} by A12, RELAT_1:149;
hence ( a in A ` implies ex f being continuous Function of T,I[01] st
( f . a = 0 & f .: A c= {1} ) ) by A13, XBOOLE_1:2; :: thesis: verum

end;

suppose not A is empty ; :: thesis: ( 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:27;
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:29;
A15: (A9 --> 1) .: A c= {1} by FUNCOP_1:96;
A16: a in aa by TARSKI:def 1;
then A17: a in B by XBOOLE_0:def 3;
assume a in A ` ; :: thesis: 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:56;
then reconsider h = ((T | A9) --> j) +* ((T | aa) --> k) as continuous Function of (T | B),(Closed-Interval-TSpace (- 1),1) by Th15;
consider g being continuous Function of T,(Closed-Interval-TSpace (- 1),1) such that
A19: g | B = h by A11, TIETZE:25;
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:42;
reconsider p9 = p /" as continuous Function of (Closed-Interval-TSpace (- 1),1),I[01] by A20, TOPS_2:def 5;
rng p = [#] (Closed-Interval-TSpace (- 1),1) by A20, TOPS_2:def 5;
then A23: p9 = p " by A20, TOPS_2:def 4;
then A24: p9 . k = z by A20, A21, FUNCT_2:32;
A25: the carrier of (T | aa) = aa by PRE_TOPC:29;
then dom ((T | aa) --> k) = aa by FUNCOP_1:19;
then A26: h . a = ((T | aa) --> k) . a by A16, FUNCT_4:14
.= - 1 by A25, A16, FUNCOP_1:13 ;
reconsider f = p9 * g as continuous Function of T,I[01] ;
A27: f .: A = p9 .: (g .: A) by RELAT_1:159
.= p9 .: (h .: A) by A19, RELAT_1:162, XBOOLE_1:7 ;
(T | A9) --> j = A9 --> 1 by PRE_TOPC:29;
then h .: A c= {1} by A14, A15, A18, BOOLMARK:3, ZFMISC_1:56;
then A28: f .: A c= Im p9,1 by A27, RELAT_1:156;
take f ; :: thesis: ( f . a = 0 & f .: A c= {1} )
thus f . a = p9 . (g . a) by FUNCT_2:21
.= 0 by A26, A17, A19, A24, FUNCT_1:72 ; :: thesis: f .: A c= {1}
p9 . j = o by A20, A22, A23, FUNCT_2:32;
hence f .: A c= {1} by A28, SETWISEO:13; :: thesis: verum

end;

end;