reconsider z = 0 as Point of I[01] by BORSUK_1:83, XXREAL_1:1;
let X be non empty T_1 TopSpace; :: thesis: for B being prebasis of X st ( for x being Point of X
for V being Subset of X st x in V & V in B holds
ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V ` ) c= {1} ) ) holds
X is Tychonoff
let BB be prebasis of X; :: thesis: ( ( for x being Point of X
for V being Subset of X st x in V & V in BB holds
ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V ` ) c= {1} ) ) implies X is Tychonoff )
assume A1: for x being Point of X
for V being Subset of X st x in V & V in BB holds
ex f being continuous Function of X,I[01] st
( f . x = 0 & f .: (V ` ) c= {1} ) ; :: thesis: X is Tychonoff
let A be closed Subset of X; :: according to TOPGEN_5:def 4 :: thesis: for a being Point of X st a in A ` holds
ex f being continuous Function of X,I[01] st
( f . a = 0 & f .: A c= {1} )
let a be Point of X; :: thesis: ( a in A ` implies ex f being continuous Function of X,I[01] st
( f . a = 0 & f .: A c= {1} ) )
A2: FinMeetCl BB is Basis of X by YELLOW_9:23;
assume a in A ` ; :: thesis: ex f being continuous Function of X,I[01] st
( f . a = 0 & f .: A c= {1} )
then consider B being Subset of X such that
A3: B in FinMeetCl BB and
A4: a in B and
A5: B c= A ` by A2, YELLOW_9:31;
consider F being Subset-Family of X such that
A6: F c= BB and
A7: F is finite and
A8: B = Intersect F by A3, CANTOR_1:def 4;

per cases ( F is empty or not F is empty ) ;

suppose F is empty ; :: thesis: ex f being continuous Function of X,I[01] st
( f . a = 0 & f .: A c= {1} )

then B = the carrier of X by A8, SETFAM_1:def 10;
then (A ` ) ` = {} X by A5, XBOOLE_1:37;
then A9: (X --> z) .: A = {} by RELAT_1:149;
(X --> z) . a = z by FUNCOP_1:13;
hence ex f being continuous Function of X,I[01] st
( f . a = 0 & f .: A c= {1} ) by A9, XBOOLE_1:2; :: thesis: verum

end;

suppose not F is empty ; :: thesis: ex f being continuous Function of X,I[01] st
( f . a = 0 & f .: A c= {1} )

then reconsider F = F as non empty finite Subset-Family of X by A7;
defpred S₁[ set , set ] means ex S being Subset of X ex f being continuous Function of X,I[01] st
( S = $1 & f = $2 & f . a = 0 & f .: (S ` ) c= {1} );
reconsider Sa = {0 } as non empty finite Subset of REAL ;
consider z being Element of F;
set R = I[01] ;
A10: for x being set st x in F holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in F implies ex y being set st S₁[x,y] )
assume A11: x in F ; :: thesis: ex y being set st S₁[x,y]
then reconsider S = x as Subset of X ;
a in S by A4, A8, A11, SETFAM_1:58;
then consider f being continuous Function of X,I[01] such that
A12: f . a = 0 and
A13: f .: (S ` ) c= {1} by A6, A11, A1;
take y = f; :: thesis: S₁[x,y]
thus S₁[x,y] by A12, A13; :: thesis: verum

end;

consider G being Function such that
A14: ( dom G = F & ( for x being set st x in F holds
S₁[x,G . x] ) ) from CLASSES1:sch 1(A10);
G is Function-yielding

proof

let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 G or G . x is set )
assume x in dom G ; :: thesis: G . x is set
then S₁[x,G . x] by A14;
hence G . x is set ; :: thesis: verum

end;

then reconsider G = G as ManySortedFunction of F by A14, PARTFUN1:def 4, RELAT_1:def 18;
rng G c= Funcs the carrier of X,the carrier of I[01]

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng G or u in Funcs the carrier of X,the carrier of I[01] )
assume u in rng G ; :: thesis: u in Funcs the carrier of X,the carrier of I[01]
then consider v being set such that
A15: v in dom G and
A16: u = G . v by FUNCT_1:def 5;
S₁[v,u] by A14, A15, A16;
hence u in Funcs the carrier of X,the carrier of I[01] by FUNCT_2:11; :: thesis: verum

end;

then G is Function of F,(Funcs the carrier of X,the carrier of I[01] ) by A14, FUNCT_2:4;
then A17: G in Funcs F,(Funcs the carrier of X,the carrier of I[01] ) by FUNCT_2:11;
then commute G in Funcs the carrier of X,(Funcs F,the carrier of I[01] ) by FUNCT_6:85;
then reconsider cG = commute G as Function of the carrier of X,(Funcs F,the carrier of I[01] ) by FUNCT_2:121;

now

let a be set ; :: thesis: ( a in F implies G . a is continuous Function of X,I[01] )
assume a in F ; :: thesis: G . a is continuous Function of X,I[01]
then S₁[a,G . a] by A14;
hence G . a is continuous Function of X,I[01] ; :: thesis: verum

end;

then consider f being continuous Function of X,I[01] such that
A18: for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute G) . x) holds
f . x = max S by Th55;
take f ; :: thesis: ( f . a = 0 & f .: A c= {1} )
reconsider cGa = cG . a as Function of F,the carrier of I[01] by FUNCT_2:121;
A19: dom cGa = F by FUNCT_2:def 1;
Sa = rng ((commute G) . a)

proof

thus Sa c= rng ((commute G) . a) :: according to XBOOLE_0:def 10 :: thesis: rng ((commute G) . a) c= Sa

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Sa or x in rng ((commute G) . a) )
assume x in Sa ; :: thesis: x in rng ((commute G) . a)
then A20: x = 0 by TARSKI:def 1;
S₁[z,G . z] by A14;
then x = ((commute G) . a) . z by A20, A17, FUNCT_6:86;
hence x in rng ((commute G) . a) by A19, FUNCT_1:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((commute G) . a) or x in Sa )
assume x in rng ((commute G) . a) ; :: thesis: x in Sa
then consider z being set such that
A21: z in dom cGa and
A22: x = cGa . z by FUNCT_1:def 5;
S₁[z,G . z] by A14, A21;
then x = 0 by A17, A21, A22, FUNCT_6:86;
hence x in Sa by TARSKI:def 1; :: thesis: verum

end;

hence f . a = max Sa by A18
.= 0 by XXREAL_2:11 ;
:: thesis: f .: A c= {1}
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in f .: A or z in {1} )
assume z in f .: A ; :: thesis: z in {1}
then consider x being set such that
A23: x in dom f and
A24: x in A and
A25: z = f . x by FUNCT_1:def 12;
reconsider x = x as Element of X by A23;
not x in B by A5, A24, XBOOLE_0:def 5;
then consider w being set such that
A26: w in F and
A27: not x in w by A8, SETFAM_1:58;
reconsider cGx = cG . x as Function of F,the carrier of I[01] by FUNCT_2:121;
reconsider S = rng cGx as non empty finite Subset of REAL by BORSUK_1:83, XBOOLE_1:1;
A28: f . x = max S by A18;
consider T being Subset of X, g being continuous Function of X,I[01] such that
A29: T = w and
A30: g = G . w and
g . a = 0 and
A31: g .: (T ` ) c= {1} by A14, A26;
x in T ` by A27, A29, SUBSET_1:50;
then g . x in g .: (T ` ) by FUNCT_2:43;
then g . x = 1 by A31, TARSKI:def 1;
then A32: cGx . w = 1 by A17, A26, A30, FUNCT_6:86;
w in dom cGx by A17, A26, A30, FUNCT_6:86;
then A33: 1 in S by A32, FUNCT_1:def 5;
for r being ext-real number st r in S holds
r <= 1 by BORSUK_1:83, XXREAL_1:1;
then max S = 1 by A33, XXREAL_2:def 8;
hence z in {1} by A25, A28, TARSKI:def 1; :: thesis: verum

end;

end;