A1: 1 in dyadic 0 by ;
then A2: 1 in DYADIC by URYSOHN1:def 2;
then 1 in () \/ DYADIC by XBOOLE_0:def 3;
then A3: 1 in DOM by ;
reconsider e1 = 1 as R_eal by XXREAL_0:def 1;
let T be non empty normal TopSpace; :: thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B holds
( Thunder G is continuous & ( for x being Point of T holds
( 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) ) ) )

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for G being Rain of A,B holds
( Thunder G is continuous & ( for x being Point of T holds
( 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) ) ) ) )

assume A4: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B holds
( Thunder G is continuous & ( for x being Point of T holds
( 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) ) ) )

let G be Rain of A,B; :: thesis: ( Thunder G is continuous & ( for x being Point of T holds
( 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) ) ) )

A5: 0 in dyadic 0 by ;
then A6: 0 in DYADIC by URYSOHN1:def 2;
then 0 in () \/ DYADIC by XBOOLE_0:def 3;
then A7: 0 in DOM by ;
A8: for x being Point of T holds
( 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) )
proof
let x be Point of T; :: thesis: ( 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) )
now :: thesis: ( ( Rainbow (x,G) = {} & 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) ) or ( Rainbow (x,G) <> {} & 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) ) )
per cases ( Rainbow (x,G) = {} or Rainbow (x,G) <> {} ) ;
case A9: Rainbow (x,G) = {} ; :: thesis: ( 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) )
( x in B implies () . x = 1 )
proof
G . 0 is Drizzle of A,B, 0 by ;
then A10: B = ([#] T) \ ((G . 0) . 1) by ;
assume A11: x in B ; :: thesis: () . x = 1
(Tempest G) . 1 = (G . 0) . 1 by A4, A1, A2, A3, Def4;
then for s being Real st s = 1 holds
not x in () . s by ;
hence (Thunder G) . x = 1 by ; :: thesis: verum
end;
hence ( 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) ) by ; :: thesis: verum
end;
case A12: Rainbow (x,G) <> {} ; :: thesis: ( 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) )
A13: ( x in A implies () . x = 0 )
proof
assume A14: x in A ; :: thesis: () . x = 0
A15: for s being R_eal st 0. < s holds
not s in Rainbow (x,G)
proof
let s be R_eal; :: thesis: ( 0. < s implies not s in Rainbow (x,G) )
assume 0. < s ; :: thesis: not s in Rainbow (x,G)
assume A16: s in Rainbow (x,G) ; :: thesis: contradiction
then A17: s in DYADIC by Def5;
then reconsider s = s as Real ;
consider n being Nat such that
A18: s in dyadic n by ;
s in () \/ DYADIC by ;
then s in DOM by ;
then A19: (Tempest G) . s = (G . n) . s by A4, A17, A18, Def4;
reconsider r1 = 0 , r2 = s as Element of dyadic n by ;
reconsider D = G . n as Drizzle of A,B,n by ;
per cases ( s = 0 or 0 < s ) by ;
suppose A21: 0 < s ; :: thesis: contradiction
A22: D . r1 c= Cl (D . r1) by PRE_TOPC:18;
Cl (D . r1) c= D . r2 by ;
then A23: D . r1 c= D . r2 by A22;
A c= D . 0 by ;
then A c= D . s by A23;
hence contradiction by A14, A16, A19, Def5; :: thesis: verum
end;
end;
end;
G . 0 is Drizzle of A,B, 0 by ;
then A24: A c= (G . 0) . 0 by ;
A25: (Tempest G) . 0 = (G . 0) . 0 by A4, A5, A6, A7, Def4;
consider a being object such that
A26: a in Rainbow (x,G) by ;
A27: a in DYADIC by ;
then reconsider a = a as Real ;
A28: ex n being Nat st a in dyadic n by ;
per cases ( a = 0 or 0 < a ) by ;
suppose a = 0 ; :: thesis: () . x = 0
hence (Thunder G) . x = 0 by A14, A25, A24, A26, Def5; :: thesis: verum
end;
suppose 0 < a ; :: thesis: () . x = 0
hence (Thunder G) . x = 0 by ; :: thesis: verum
end;
end;
end;
reconsider S = Rainbow (x,G) as non empty Subset of ExtREAL by A12;
A29: sup S <= e1 by Th14;
A30: ( x in B implies () . x = 1 )
proof
G . 0 is Drizzle of A,B, 0 by ;
then A31: B = ([#] T) \ ((G . 0) . 1) by ;
assume A32: x in B ; :: thesis: () . x = 1
(Tempest G) . 1 = (G . 0) . 1 by A4, A1, A2, A3, Def4;
then A33: for s being Real st s = 1 holds
not x in () . s by ;
then reconsider S = Rainbow (x,G) as non empty Subset of ExtREAL by ;
1 in Rainbow (x,G) by ;
then A34: e1 <= sup S by XXREAL_2:4;
(Thunder G) . x = sup S by Def6;
hence (Thunder G) . x = 1 by ; :: thesis: verum
end;
( e1 = 1 & () . x = sup S ) by Def6;
hence ( 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) ) by ; :: thesis: verum
end;
end;
end;
hence ( 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) ) ; :: thesis: verum
end;
for p being Point of T holds Thunder G is_continuous_at p
proof
let p be Point of T; :: thesis:
for Q being Subset of R^1 st Q is open & () . p in Q holds
ex H being Subset of T st
( H is open & p in H & () .: H c= Q )
proof
let Q be Subset of R^1; :: thesis: ( Q is open & () . p in Q implies ex H being Subset of T st
( H is open & p in H & () .: H c= Q ) )

assume that
A35: Q is open and
A36: (Thunder G) . p in Q ; :: thesis: ex H being Subset of T st
( H is open & p in H & () .: H c= Q )

reconsider x = () . p as Element of RealSpace by ;
reconsider Q = Q as Subset of REAL by TOPMETR:17;
( the topology of R^1 = Family_open_set RealSpace & Q in the topology of R^1 ) by ;
then consider r being Real such that
A37: r > 0 and
A38: Ball (x,r) c= Q by ;
ex r0 being Real st
( r0 < r & 0 < r0 & r0 <= 1 )
proof
per cases ( r <= 1 or 1 < r ) ;
suppose A39: r <= 1 ; :: thesis: ex r0 being Real st
( r0 < r & 0 < r0 & r0 <= 1 )

consider r0 being Real such that
A40: ( 0 < r0 & r0 < r ) by ;
reconsider r0 = r0 as Real ;
take r0 ; :: thesis: ( r0 < r & 0 < r0 & r0 <= 1 )
thus ( r0 < r & 0 < r0 & r0 <= 1 ) by ; :: thesis: verum
end;
suppose 1 < r ; :: thesis: ex r0 being Real st
( r0 < r & 0 < r0 & r0 <= 1 )

hence ex r0 being Real st
( r0 < r & 0 < r0 & r0 <= 1 ) ; :: thesis: verum
end;
end;
end;
then consider r0 being Real such that
A41: r0 < r and
A42: ( 0 < r0 & r0 <= 1 ) ;
consider r1 being Real such that
A43: r1 in DYADIC and
A44: 0 < r1 and
A45: r1 < r0 by ;
A46: r1 in DYADIC \/ by ;
consider n being Nat such that
A47: r1 in dyadic n by ;
reconsider D = G . n as Drizzle of A,B,n by ;
r1 in () \/ DYADIC by ;
then A48: r1 in DOM by ;
then A49: (Tempest G) . r1 = (G . n) . r1 by A4, A43, A47, Def4;
A50: r1 < r by ;
A51: for p being Point of T st p in () . r1 holds
() . p < r
proof
let p be Point of T; :: thesis: ( p in () . r1 implies () . p < r )
assume p in () . r1 ; :: thesis: () . p < r
then (Thunder G) . p <= r1 by A4, A44, A46, Th16;
hence (Thunder G) . p < r by ; :: thesis: verum
end;
A52: the carrier of R^1 = the carrier of RealSpace by ;
reconsider r1 = r1 as Element of dyadic n by A47;
reconsider H = D . r1 as Subset of T ;
A53: 0 in dyadic n by URYSOHN1:6;
ex H being Subset of T st
( H is open & p in H & () .: H c= Q )
proof
per cases ( x = 0 or x <> 0 ) ;
suppose A54: x = 0 ; :: thesis: ex H being Subset of T st
( H is open & p in H & () .: H c= Q )

take H ; :: thesis: ( H is open & p in H & () .: H c= Q )
(Thunder G) .: H c= Q
proof
reconsider p = x as Real ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in () .: H or y in Q )
assume y in () .: H ; :: thesis: y in Q
then consider x1 being object such that
x1 in dom () and
A55: x1 in H and
A56: y = () . x1 by FUNCT_1:def 6;
reconsider y = y as Point of RealSpace by ;
reconsider q = y as Real ;
A57: - (p - q) < r by A51, A49, A54, A55, A56;
reconsider x1 = x1 as Point of T by A55;
A58: 0 <= () . x1 by A8;
A59: q - p < r - 0 by A51, A49, A54, A55, A56;
then p - q < r by ;
then A60: |.(p - q).| <> r by ;
A61: ( dist (x,y) < r implies y in Ball (x,r) ) by METRIC_1:11;
- (- (p - q)) = p - q ;
then - r < p - q by ;
then ( dist (x,y) = |.(p - q).| & |.(p - q).| <= r ) by ;
hence y in Q by ; :: thesis: verum
end;
hence ( H is open & p in H & () .: H c= Q ) by A4, A44, A48, A49, A53, A54, Def1, Th15; :: thesis: verum
end;
suppose A62: x <> 0 ; :: thesis: ex H being Subset of T st
( H is open & p in H & () .: H c= Q )

reconsider x = x as Real ;
0 <= () . p by A8;
then consider r1, r2 being Real such that
A63: r1 in DYADIC \/ and
r2 in DYADIC \/ and
A64: 0 < r1 and
A65: r1 < x and
A66: x < r2 and
A67: r2 - r1 < r by ;
( r1 in DYADIC or r1 in right_open_halfline 1 ) by ;
then ( r1 in () \/ DYADIC or r1 in right_open_halfline 1 ) by XBOOLE_0:def 3;
then A68: r1 in DOM by ;
then reconsider B = () . r1 as Subset of T by FUNCT_2:5;
reconsider C = ([#] T) \ (Cl B) as Subset of T ;
consider r3 being Real such that
A69: r3 in DOM and
A70: x < r3 and
A71: r3 < r2 by ;
Cl (Cl B) = Cl B ;
then Cl B is closed by PRE_TOPC:22;
then A72: C is open ;
reconsider A = () . r3 as Subset of T by ;
take H = A /\ C; :: thesis: ( H is open & p in H & () .: H c= Q )
A73: (Thunder G) .: H c= Q
proof
reconsider x = x as Element of RealSpace ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in () .: H or y in Q )
reconsider p = x as Real ;
assume y in () .: H ; :: thesis: y in Q
then consider x1 being object such that
x1 in dom () and
A74: x1 in H and
A75: y = () . x1 by FUNCT_1:def 6;
reconsider x1 = x1 as Point of T by A74;
A76: x1 in () . r3 by ;
reconsider y = y as Real by A75;
reconsider y = y as Point of RealSpace by ;
reconsider q = y as Real ;
A77: - (- (p - q)) = p - q ;
A78: not r3 <= 0 by ;
( r3 in () \/ DYADIC or r3 in right_open_halfline 1 ) by ;
then ( r3 in halfline 0 or r3 in DYADIC or r3 in right_open_halfline 1 ) by XBOOLE_0:def 3;
then r3 in DYADIC \/ by ;
then (Thunder G) . x1 <= r3 by A4, A76, A78, Th16;
then (Thunder G) . x1 < r2 by ;
then A79: q - p < r2 - r1 by ;
then - (p - q) < r by ;
then A80: - r < p - q by ;
A81: x1 in ([#] T) \ (Cl B) by ;
not x1 in B then A83: p - q < r2 - r1 by ;
then p - q < r by ;
then A84: ( dist (x,y) = |.(p - q).| & |.(p - q).| <= r ) by ;
A85: |.(p - q).| <> r
proof
assume A86: |.(p - q).| = r ; :: thesis: contradiction
per cases ( 0 <= p - q or p - q < 0 ) ;
end;
end;
( dist (x,y) < r implies y in Ball (x,r) ) by METRIC_1:11;
hence y in Q by ; :: thesis: verum
end;
(Thunder G) . p <= 1 by A8;
then consider r4 being Real such that
A87: r4 in DYADIC and
A88: r1 < r4 and
A89: r4 < x by ;
A90: r4 in () \/ DYADIC by ;
then r4 in DOM by ;
then A91: Cl B c= () . r4 by A4, A88, A68, Th12;
reconsider r4 = r4 as Element of DOM by ;
not p in () . r4 by A4, A64, A88, A89, Th17;
then not p in Cl B by A91;
then A92: p in C by XBOOLE_0:def 5;
( A is open & p in () . r3 ) by A4, A69, A70, Th11, Th15;
hence ( H is open & p in H & () .: H c= Q ) by ; :: thesis: verum
end;
end;
end;
hence ex H being Subset of T st
( H is open & p in H & () .: H c= Q ) ; :: thesis: verum
end;
hence Thunder G is_continuous_at p by TMAP_1:43; :: thesis: verum
end;
hence ( Thunder G is continuous & ( for x being Point of T holds
( 0 <= () . x & () . x <= 1 & ( x in A implies () . x = 0 ) & ( x in B implies () . x = 1 ) ) ) ) by ; :: thesis: verum