reconsider z = 0 as Point of I[01] by BORSUK_1:40, 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 3;
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 9;
then (A `) ` = {} X by A5, XBOOLE_1:37;
then A9: (X --> z) .: A = {} ;
(X --> z) . a = z ;
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 S1[ object , object ] 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 = {(In (0,REAL))} as non empty finite Subset of REAL ;
set z = the Element of F;
set R = I[01] ;
A10: for x being object st x in F holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in F implies ex y being object st S1[x,y] )
assume A11: x in F ; :: thesis: ex y being object st S1[x,y]
then reconsider S = x as Subset of X ;
a in S by A4, A8, A11, SETFAM_1:43;
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 f ; :: thesis: S1[x,f]
thus S1[x,f] by A12, A13; :: thesis: verum
end;
consider G being Function such that
A14: ( dom G = F & ( for x being object st x in F holds
S1[x,G . x] ) ) from CLASSES1:sch 1(A10);
 G is Function-yielding
proof
let x be object ; :: 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 S1[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 2, RELAT_1:def 18;
rng G c= Funcs ( the carrier of X, the carrier of I[01])
proof
let u be object ; :: 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 object such that
A15: v in dom G and
A16: u = G . v by FUNCT_1:def 3;
S1[v,u] by A14, A15, A16;
hence u in Funcs ( the carrier of X, the carrier of I[01]) by FUNCT_2:8; :: thesis: verum
end;
then G is Function of F,(Funcs ( the carrier of X, the carrier of I[01])) by A14, FUNCT_2:2;
then A17: G in Funcs (F,(Funcs ( the carrier of X, the carrier of I[01]))) by FUNCT_2:8;
then commute G in Funcs ( the carrier of X,(Funcs (F, the carrier of I[01]))) by FUNCT_6:55;
then reconsider cG = commute G as Function of the carrier of X,(Funcs (F, the carrier of I[01])) by FUNCT_2:66;
now :: thesis: for a being set st a in F holds
G . a is continuous Function of X,I[01]
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 S1[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 Th51;
take f ; :: thesis: ( f . a = 0 & f .: A c= {1} )
reconsider cGa = cG . a as Function of F, the carrier of I[01] ;
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 object ; :: 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;
S1[ the Element of F,G . the Element of F] by A14;
then x = ((commute G) . a) . the Element of F by A20, A17, FUNCT_6:56;
hence x in rng ((commute G) . a) by A19, FUNCT_1:def 3; :: thesis: verum
end;
let x be object ; :: 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 object such that
A21: z in dom cGa and
A22: x = cGa . z by FUNCT_1:def 3;
S1[z,G . z] by A14, A21;
then x = 0 by A17, A21, A22, FUNCT_6:56;
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 object ; :: 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 object such that
A23: x in dom f and
A24: x in A and
A25: z = f . x by FUNCT_1:def 6;
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:43;
reconsider cGx = cG . x as Function of F, the carrier of I[01] ;
reconsider S = rng cGx as non empty finite Subset of REAL by BORSUK_1:40, 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:29;
then g . x in g .: (T `) by FUNCT_2:35;
then g . x = 1 by A31, TARSKI:def 1;
then A32: cGx . w = 1 by A17, A26, A30, FUNCT_6:56;
w in dom cGx by A17, A26, A30, FUNCT_6:56;
then A33: 1 in S by A32, FUNCT_1:def 3;
for r being ExtReal st r in S holds
r <= 1 by BORSUK_1:40, 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;