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

proof

let x be Point of T; :: thesis:

now :: thesis:

per cases ;

case A9: Rainbow (x,G) = {} ; :: thesis:

( x in B implies (Thunder G) . x = 1 )

proof

G . 0 is Drizzle of A,B, 0 by A4, Def2;
then A10: B = ([#] T) \ ((G . 0) . 1) by A4, Def1;
assume A11: x in B ; :: thesis:
(Tempest G) . 1 = (G . 0) . 1 by A4, A1, A2, A3, Def4;
then for s being Real st s = 1 holds
not x in (Tempest G) . s by A11, A10, XBOOLE_0:def 5;
hence (Thunder G) . x = 1 by A9, Def5, URYSOHN2:27; :: thesis:

end;

hence ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) by A9, Def6; :: thesis:

end;

case A12: Rainbow (x,G) <> {} ; :: thesis:

A13: ( x in A implies (Thunder G) . x = 0 )

proof

assume A14: x in A ; :: thesis:
A15: for s being R_eal st 0. < s holds
not s in Rainbow (x,G)

proof

let s be R_eal; :: thesis:
assume 0. < s ; :: thesis:
assume A16: s in Rainbow (x,G) ; :: thesis:
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 A17, URYSOHN1:def 2;
s in (halfline 0) \/ DYADIC by A17, XBOOLE_0:def 3;
then s in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;
then A19: (Tempest G) . s = (G . n) . s by A4, A17, A18, Def4;
reconsider r1 = 0 , r2 = s as Element of dyadic n by A18, URYSOHN1:6;
reconsider D = G . n as Drizzle of A,B,n by A4, Def2;

per cases by A18, URYSOHN1:1;

suppose A20: s = 0 ; :: thesis:

A c= D . 0 by A4, Def1;
hence contradiction by A14, A16, A19, A20, Def5; :: thesis:

end;

suppose A21: 0 < s ; :: thesis:

A22: D . r1 c= Cl (D . r1) by PRE_TOPC:18;
Cl (D . r1) c= D . r2 by A4, A21, Def1;
then A23: D . r1 c= D . r2 by A22;
A c= D . 0 by A4, Def1;
then A c= D . s by A23;
hence contradiction by A14, A16, A19, Def5; :: thesis:

end;

G . 0 is Drizzle of A,B, 0 by A4, Def2;
then A24: A c= (G . 0) . 0 by A4, Def1;
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 A12, XBOOLE_0:def 1;
A27: a in DYADIC by A26, Def5;
then reconsider a = a as Real ;
A28: ex n being Nat st a in dyadic n by A27, URYSOHN1:def 2;

per cases by A28, URYSOHN1:1;

suppose a = 0 ; :: thesis:

hence (Thunder G) . x = 0 by A14, A25, A24, A26, Def5; :: thesis:

end;

suppose 0 < a ; :: thesis:

hence (Thunder G) . x = 0 by A15, A26; :: thesis:

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 (Thunder G) . x = 1 )

proof

G . 0 is Drizzle of A,B, 0 by A4, Def2;
then A31: B = ([#] T) \ ((G . 0) . 1) by A4, Def1;
assume A32: x in B ; :: thesis:
(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 (Tempest G) . s by A32, A31, XBOOLE_0:def 5;
then reconsider S = Rainbow (x,G) as non empty Subset of ExtREAL by Def5, URYSOHN2:27;
1 in Rainbow (x,G) by A33, Def5, URYSOHN2:27;
then A34: e1 <= sup S by XXREAL_2:4;
(Thunder G) . x = sup S by Def6;
hence (Thunder G) . x = 1 by A29, A34, XXREAL_0:1; :: thesis:

end;

( e1 = 1 & (Thunder G) . x = sup S ) by Def6;
hence ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) by A13, A30, Th14; :: thesis:

end;

hence ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ; :: thesis:

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 & (Thunder G) . p in Q holds
ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q )

proof

let Q be Subset of R^1; :: thesis:
assume that
A35: Q is open and
A36: (Thunder G) . p in Q ; :: thesis:
reconsider x = (Thunder G) . p as Element of RealSpace by A36, TOPMETR:12, TOPMETR:def 6;
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 A35, TOPMETR:12, TOPMETR:def 6;
then consider r being Real such that
A37: r > 0 and
A38: Ball (x,r) c= Q by A36, PCOMPS_1:def 4;
ex r0 being Real st
( r0 < r & 0 < r0 & r0 <= 1 )

proof

per cases ;

suppose A39: r <= 1 ; :: thesis:

consider r0 being Real such that
A40: ( 0 < r0 & r0 < r ) by A37, XREAL_1:5;
reconsider r0 = r0 as Real ;
take r0 ; :: thesis:
thus ( r0 < r & 0 < r0 & r0 <= 1 ) by A39, A40, XXREAL_0:2; :: thesis:

end;

suppose 1 < r ; :: thesis:

hence ex r0 being Real st
( r0 < r & 0 < r0 & r0 <= 1 ) ; :: thesis:

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 A42, URYSOHN2:24;
A46: r1 in DYADIC \/ (right_open_halfline 1) by A43, XBOOLE_0:def 3;
consider n being Nat such that
A47: r1 in dyadic n by A43, URYSOHN1:def 2;
reconsider D = G . n as Drizzle of A,B,n by A4, Def2;
r1 in (halfline 0) \/ DYADIC by A43, XBOOLE_0:def 3;
then A48: r1 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;
then A49: (Tempest G) . r1 = (G . n) . r1 by A4, A43, A47, Def4;
A50: r1 < r by A41, A45, XXREAL_0:2;
A51: for p being Point of T st p in (Tempest G) . r1 holds
(Thunder G) . p < r

proof

let p be Point of T; :: thesis:
assume p in (Tempest G) . r1 ; :: thesis:
then (Thunder G) . p <= r1 by A4, A44, A46, Th16;
hence (Thunder G) . p < r by A50, XXREAL_0:2; :: thesis:

end;

A52: the carrier of R^1 = the carrier of RealSpace by TOPMETR:12, TOPMETR:def 6;
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 & (Thunder G) .: H c= Q )

proof

per cases ;

suppose A54: x = 0 ; :: thesis:

take H ; :: thesis:
(Thunder G) .: H c= Q

proof

reconsider p = x as Real ;
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in (Thunder G) .: H ; :: thesis:
then consider x1 being object such that
x1 in dom (Thunder G) and
A55: x1 in H and
A56: y = (Thunder G) . x1 by FUNCT_1:def 6;
reconsider y = y as Point of RealSpace by A52, A55, A56, FUNCT_2:5;
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 <= (Thunder G) . x1 by A8;
A59: q - p < r - 0 by A51, A49, A54, A55, A56;
then p - q < r by A54, A56, A58, XREAL_1:14;
then A60: |.(p - q).| <> r by A57, ABSVALUE:def 1;
A61: ( dist (x,y) < r implies y in Ball (x,r) ) by METRIC_1:11;
- (- (p - q)) = p - q ;
then - r < p - q by A57, XREAL_1:24;
then ( dist (x,y) = |.(p - q).| & |.(p - q).| <= r ) by A54, A56, A58, A59, ABSVALUE:5, TOPMETR:11;
hence y in Q by A38, A61, A60, XXREAL_0:1; :: thesis:

end;

hence ( H is open & p in H & (Thunder G) .: H c= Q ) by A4, A44, A48, A49, A53, A54, Def1, Th15; :: thesis:

end;

suppose A62: x <> 0 ; :: thesis:

reconsider x = x as Real ;
0 <= (Thunder G) . p by A8;
then consider r1, r2 being Real such that
A63: r1 in DYADIC \/ (right_open_halfline 1) and
r2 in DYADIC \/ (right_open_halfline 1) and
A64: 0 < r1 and
A65: r1 < x and
A66: x < r2 and
A67: r2 - r1 < r by A37, A62, URYSOHN2:31;
( r1 in DYADIC or r1 in right_open_halfline 1 ) by A63, XBOOLE_0:def 3;
then ( r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 ) by XBOOLE_0:def 3;
then A68: r1 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;
then reconsider B = (Tempest G) . 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 A66, URYSOHN2:25;
Cl (Cl B) = Cl B ;
then Cl B is closed by PRE_TOPC:22;
then A72: C is open ;
reconsider A = (Tempest G) . r3 as Subset of T by A69, FUNCT_2:5;
take H = A /\ C; :: thesis:
A73: (Thunder G) .: H c= Q

proof

reconsider x = x as Element of RealSpace ;
let y be object ; :: according to TARSKI:def 3 :: thesis:
reconsider p = x as Real ;
assume y in (Thunder G) .: H ; :: thesis:
then consider x1 being object such that
x1 in dom (Thunder G) and
A74: x1 in H and
A75: y = (Thunder G) . x1 by FUNCT_1:def 6;
reconsider x1 = x1 as Point of T by A74;
A76: x1 in (Tempest G) . r3 by A74, XBOOLE_0:def 4;
reconsider y = y as Real by A75;
reconsider y = y as Point of RealSpace by A52, A74, A75, FUNCT_2:5;
reconsider q = y as Real ;
A77: - (- (p - q)) = p - q ;
A78: not r3 <= 0 by A8, A70;
( r3 in (halfline 0) \/ DYADIC or r3 in right_open_halfline 1 ) by A69, URYSOHN1:def 3, XBOOLE_0:def 3;
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 \/ (right_open_halfline 1) by A78, XBOOLE_0:def 3, XXREAL_1:233;
then (Thunder G) . x1 <= r3 by A4, A76, A78, Th16;
then (Thunder G) . x1 < r2 by A71, XXREAL_0:2;
then A79: q - p < r2 - r1 by A65, A75, XREAL_1:14;
then - (p - q) < r by A67, XXREAL_0:2;
then A80: - r < p - q by A77, XREAL_1:24;
A81: x1 in ([#] T) \ (Cl B) by A74, XBOOLE_0:def 4;
not x1 in B

proof

A82: B c= Cl B by PRE_TOPC:18;
assume x1 in B ; :: thesis:
hence contradiction by A81, A82, XBOOLE_0:def 5; :: thesis:

end;

then A83: p - q < r2 - r1 by A4, A66, A68, A75, Th15, XREAL_1:14;
then p - q < r by A67, XXREAL_0:2;
then A84: ( dist (x,y) = |.(p - q).| & |.(p - q).| <= r ) by A80, ABSVALUE:5, TOPMETR:11;
A85: |.(p - q).| <> r

proof

assume A86: |.(p - q).| = r ; :: thesis:

per cases ;

suppose 0 <= p - q ; :: thesis:

hence contradiction by A67, A83, A86, ABSVALUE:def 1; :: thesis:

end;

suppose p - q < 0 ; :: thesis:

then |.(p - q).| = - (p - q) by ABSVALUE:def 1;
hence contradiction by A67, A79, A86; :: thesis:

end;

( dist (x,y) < r implies y in Ball (x,r) ) by METRIC_1:11;
hence y in Q by A38, A84, A85, XXREAL_0:1; :: thesis:

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 A64, A65, URYSOHN2:24;
A90: r4 in (halfline 0) \/ DYADIC by A87, XBOOLE_0:def 3;
then r4 in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;
then A91: Cl B c= (Tempest G) . r4 by A4, A88, A68, Th12;
reconsider r4 = r4 as Element of DOM by A90, URYSOHN1:def 3, XBOOLE_0:def 3;
not p in (Tempest G) . 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 (Tempest G) . r3 ) by A4, A69, A70, Th11, Th15;
hence ( H is open & p in H & (Thunder G) .: H c= Q ) by A72, A92, A73, TOPS_1:11, XBOOLE_0:def 4; :: thesis:

end;

hence ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q ) ; :: thesis:

end;

hence Thunder G is_continuous_at p by TMAP_1:43; :: thesis:

end;

hence ( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) ) by A8, TMAP_1:44; :: thesis: