let T be non empty normal TopSpace; :: thesis:
let A, B be closed Subset of T; :: thesis:
assume A1: ( A <> {} & A misses B ) ; :: thesis:
let G be Rain of A,B; :: thesis:
reconsider e1 = 1 as R_eal by XXREAL_0:def 1;
A2: 1 in dyadic 0 by TARSKI:def 2, URYSOHN1:6;
then A3: 1 in DYADIC by URYSOHN1:def 4;
then 1 in (halfline 0 ) \/ DYADIC by XBOOLE_0:def 3;
then A4: 1 in DOM by URYSOHN1:def 5, XBOOLE_0:def 3;
A5: 0 in dyadic 0 by TARSKI:def 2, URYSOHN1:6;
then A6: 0 in DYADIC by URYSOHN1:def 4;
then 0 in (halfline 0 ) \/ DYADIC by XBOOLE_0:def 3;
then A7: 0 in DOM by URYSOHN1:def 5, 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

per cases ;

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

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

proof

assume A10: x in B ; :: thesis:
A11: (Tempest G) . 1 = (G . 0 ) . 1 by A1, A2, A3, A4, Def4;
( G . 0 is Drizzle of A,B, 0 & ( for r being Element of dom (G . 0 ) holds (G . 0 ) . r = (G . (0 + 1)) . r ) ) by A1, Def2;
then B = ([#] T) \ ((G . 0 ) . 1) by A1, Def1;
then for s being Real st s = 1 holds
not x in (Tempest G) . s by A10, A11, XBOOLE_0:def 5;
hence (Thunder G) . x = 1 by A9, Def5, URYSOHN2:31; :: 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:

then reconsider S = Rainbow x,G as non empty Subset of ExtREAL ;
A13: e1 = 1 ;
then A14: ( 0. <= sup S & sup S <= e1 ) by Th17;
A15: ( (Thunder G) . x = sup S & 0. = 0 ) by Def6;
A16: ( x in A implies (Thunder G) . x = 0 )

proof

assume A17: x in A ; :: thesis:
A18: (Tempest G) . 0 = (G . 0 ) . 0 by A1, A5, A6, A7, Def4;
( G . 0 is Drizzle of A,B, 0 & ( for r being Element of dom (G . 0 ) holds (G . 0 ) . r = (G . (0 + 1)) . r ) ) by A1, Def2;
then A19: A c= (G . 0 ) . 0 by A1, Def1;
A20: 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 A21: s in Rainbow x,G ; :: thesis:
then A22: ( s in DYADIC & ( for t being Real st t = s holds
not x in (Tempest G) . t ) ) by Def5;
then reconsider s = s as Real ;
s in (halfline 0 ) \/ DYADIC by A22, XBOOLE_0:def 3;
then A23: s in DOM by URYSOHN1:def 5, XBOOLE_0:def 3;
consider n being Element of NAT such that
A24: s in dyadic n by A22, URYSOHN1:def 4;
A25: (Tempest G) . s = (G . n) . s by A1, A22, A23, A24, Def4;
reconsider D = G . n as Drizzle of A,B,n by A1, Def2;
reconsider r1 = 0 , r2 = s as Element of dyadic n by A24, URYSOHN1:12;

per cases by A24, URYSOHN1:5;

suppose A26: s = 0 ; :: thesis:

A c= D . 0 by A1, Def1;
hence contradiction by A17, A21, A25, A26, Def5; :: thesis:

end;

suppose 0 < s ; :: thesis:

then A27: ( Cl (D . r1) c= D . r2 & A c= D . 0 ) by A1, Def1;
D . r1 c= Cl (D . r1) by PRE_TOPC:48;
then D . r1 c= D . r2 by A27, XBOOLE_1:1;
then A c= D . s by A27, XBOOLE_1:1;
hence contradiction by A17, A21, A25, Def5; :: thesis:

end;

consider a being set such that
A28: a in Rainbow x,G by A12, XBOOLE_0:def 1;
A29: a in DYADIC by A28, Def5;
then reconsider a = a as Real ;
consider n being Element of NAT such that
A30: a in dyadic n by A29, URYSOHN1:def 4;

per cases by A30, URYSOHN1:5;

suppose a = 0 ; :: thesis:

hence (Thunder G) . x = 0 by A17, A18, A19, A28, Def5; :: thesis:

end;

suppose 0 < a ; :: thesis:

hence (Thunder G) . x = 0 by A20, A28; :: thesis:

end;

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

proof

assume A31: x in B ; :: thesis:
A32: (Tempest G) . 1 = (G . 0 ) . 1 by A1, A2, A3, A4, Def4;
( G . 0 is Drizzle of A,B, 0 & ( for r being Element of dom (G . 0 ) holds (G . 0 ) . r = (G . (0 + 1)) . r ) ) by A1, Def2;
then B = ([#] T) \ ((G . 0 ) . 1) by A1, Def1;
then A33: for s being Real st s = 1 holds
not x in (Tempest G) . s by A31, A32, XBOOLE_0:def 5;
then A34: 1 in Rainbow x,G by Def5, URYSOHN2:31;
reconsider S = Rainbow x,G as non empty Subset of ExtREAL by A33, Def5, URYSOHN2:31;
A35: e1 <= sup S by A34, XXREAL_2:4;
(Thunder G) . x = sup S by Def6;
hence (Thunder G) . x = 1 by A14, A35, XXREAL_0:1; :: 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 A13, A15, A16, Th17; :: 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;

Thunder G is continuous

proof

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 A36: ( Q is open & (Thunder G) . p in Q ) ; :: thesis:
reconsider Q = Q as Subset of REAL by TOPMETR:24;
A37: ( the carrier of R^1 = the carrier of RealSpace & the topology of R^1 = Family_open_set RealSpace ) by TOPMETR:16, TOPMETR:def 7;
A38: Q in the topology of R^1 by A36, PRE_TOPC:def 5;
reconsider x = (Thunder G) . p as Element of RealSpace by A36, TOPMETR:16, TOPMETR:def 7;
consider r being Real such that
A39: ( r > 0 & Ball x,r c= Q ) by A36, A37, A38, PCOMPS_1:def 5;
ex r0 being Real st
( r0 < r & 0 < r0 & r0 <= 1 )

proof

per cases ;

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

consider r0 being real number such that
A41: ( 0 < r0 & r0 < r ) by A39, XREAL_1:7;
reconsider r0 = r0 as Real by XREAL_0:def 1;
take r0 ; :: thesis:
thus ( r0 < r & 0 < r0 & r0 <= 1 ) by A40, A41, 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
A42: ( r0 < r & 0 < r0 & r0 <= 1 ) ;
consider r1 being Real such that
A43: ( r1 in DYADIC & 0 < r1 & r1 < r0 ) by A42, URYSOHN2:28;
A44: r1 < r by A42, A43, XXREAL_0:2;
A45: ( r1 in DYADIC \/ (right_open_halfline 1) & 0 < r1 ) by A43, XBOOLE_0:def 3;
A46: 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 A1, A45, Th19;
hence (Thunder G) . p < r by A44, XXREAL_0:2; :: thesis:

end;

consider n being Element of NAT such that
A47: r1 in dyadic n by A43, URYSOHN1:def 4;
r1 in (halfline 0 ) \/ DYADIC by A43, XBOOLE_0:def 3;
then A48: r1 in DOM by URYSOHN1:def 5, XBOOLE_0:def 3;
then A49: (Tempest G) . r1 = (G . n) . r1 by A1, A43, A47, Def4;
reconsider D = G . n as Drizzle of A,B,n by A1, Def2;
A50: ( 0 in dyadic n & r1 in dyadic n & 0 < r1 ) by A43, A47, URYSOHN1:12;
reconsider r1 = r1 as Element of dyadic n by A47;
reconsider H = D . r1 as Subset of T ;
ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q )

proof

per cases ;

suppose A51: x = 0 ; :: thesis:

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in (Thunder G) .: H ; :: thesis:
then consider x1 being set such that
A52: ( x1 in dom (Thunder G) & x1 in H & y = (Thunder G) . x1 ) by FUNCT_1:def 12;
reconsider x1 = x1 as Point of T by A52;
A53: 0 <= (Thunder G) . x1 by A8;
reconsider p = x as Real ;
reconsider y = y as Point of RealSpace by A37, A52, FUNCT_2:7;
reconsider q = y as Real by METRIC_1:def 14;
A54: dist x,y = abs (p - q) by TOPMETR:15;
A55: ( dist x,y < r implies y in Ball x,r ) by METRIC_1:12;
q - p < r - 0 by A46, A49, A51, A52;
then A56: ( p - q < r & - (p - q) < r ) by A51, A52, A53, XREAL_1:16;
- (- (p - q)) = p - q ;
then ( - r < p - q & p - q < r ) by A56, XREAL_1:26;
then A57: abs (p - q) <= r by ABSVALUE:12;
abs (p - q) <> r

proof

assume A58: abs (p - q) = r ; :: thesis:

per cases ;

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

thus contradiction by A56, A58, ABSVALUE:def 1; :: thesis:

end;

suppose p - q < 0 ; :: thesis:

then abs (p - q) = - (p - q) by ABSVALUE:def 1;
hence contradiction by A46, A49, A51, A52, A58; :: thesis:

end;

hence y in Q by A39, A54, A55, A57, XXREAL_0:1; :: thesis:

end;

hence ( H is open & p in H & (Thunder G) .: H c= Q ) by A1, A48, A49, A50, A51, Def1, Th18; :: thesis:

end;

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

A60: ( 0 <= (Thunder G) . p & (Thunder G) . p <= 1 ) by A8;
reconsider x = x as Real ;
consider r1, r2 being Real such that
A61: ( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < x & x < r2 & r2 - r1 < r ) by A39, A59, A60, URYSOHN2:35;
consider r4 being Real such that
A62: ( r4 in DYADIC & r1 < r4 & r4 < x ) by A60, A61, URYSOHN2:28;
consider r3 being Real such that
A63: ( r3 in DOM & x < r3 & r3 < r2 ) by A61, URYSOHN2:29;
reconsider A = (Tempest G) . r3 as Subset of T by A63, FUNCT_2:7;
A64: A is open by A1, A63, Th12;
( r1 in DYADIC or r1 in right_open_halfline 1 ) by A61, XBOOLE_0:def 3;
then ( r1 in (halfline 0 ) \/ DYADIC or r1 in right_open_halfline 1 ) by XBOOLE_0:def 3;
then A65: r1 in DOM by URYSOHN1:def 5, XBOOLE_0:def 3;
then reconsider B = (Tempest G) . r1 as Subset of T by FUNCT_2:7;
reconsider C = ([#] T) \ (Cl B) as Subset of T ;
Cl (Cl B) = Cl B ;
then Cl B is closed by PRE_TOPC:52;
then A66: C is open by PRE_TOPC:def 6;
take H = A /\ C; :: thesis:
A67: r4 in (halfline 0 ) \/ DYADIC by A62, XBOOLE_0:def 3;
then r4 in DOM by URYSOHN1:def 5, XBOOLE_0:def 3;
then A68: Cl B c= (Tempest G) . r4 by A1, A62, A65, Th13;
reconsider r4 = r4 as Element of DOM by A67, URYSOHN1:def 5, XBOOLE_0:def 3;
not p in (Tempest G) . r4 by A1, A61, A62, Th20;
then not p in Cl B by A68;
then A69: p in C by XBOOLE_0:def 5;
A70: p in (Tempest G) . r3 by A1, A63, Th18;
(Thunder G) .: H c= Q

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in (Thunder G) .: H ; :: thesis:
then consider x1 being set such that
A71: ( x1 in dom (Thunder G) & x1 in H & y = (Thunder G) . x1 ) by FUNCT_1:def 12;
reconsider x1 = x1 as Point of T by A71;
reconsider y = y as Real by A71;
A72: ( x1 in (Tempest G) . r3 & x1 in ([#] T) \ (Cl B) ) by A71, XBOOLE_0:def 4;
not x1 in B

proof

assume A73: x1 in B ; :: thesis:
B c= Cl B by PRE_TOPC:48;
hence contradiction by A72, A73, XBOOLE_0:def 5; :: thesis:

end;

then A74: r1 <= (Thunder G) . x1 by A1, A65, Th18;
( ( r3 in (halfline 0 ) \/ DYADIC or r3 in right_open_halfline 1 ) & not r3 <= 0 ) by A8, A63, URYSOHN1:def 5, XBOOLE_0:def 3;
then ( ( r3 in halfline 0 or r3 in DYADIC or r3 in right_open_halfline 1 ) & not r3 <= 0 ) by XBOOLE_0:def 3;
then ( r3 in DYADIC \/ (right_open_halfline 1) & 0 < r3 ) by XBOOLE_0:def 3, XXREAL_1:233;
then (Thunder G) . x1 <= r3 by A1, A72, Th19;
then A75: (Thunder G) . x1 < r2 by A63, XXREAL_0:2;
reconsider x = x as Element of RealSpace ;
reconsider p = x as Real ;
reconsider y = y as Point of RealSpace by A37, A71, FUNCT_2:7;
reconsider q = y as Real ;
A76: dist x,y = abs (p - q) by TOPMETR:15;
A77: ( dist x,y < r implies y in Ball x,r ) by METRIC_1:12;
A78: q - p < r2 - r1 by A61, A71, A75, XREAL_1:16;
A79: p - q < r2 - r1 by A61, A71, A74, XREAL_1:16;
then A80: ( p - q < r & - (p - q) < r ) by A61, A78, XXREAL_0:2;
- (- (p - q)) = p - q ;
then ( - r < p - q & p - q < r ) by A80, XREAL_1:26;
then A81: abs (p - q) <= r by ABSVALUE:12;
abs (p - q) <> r

proof

assume A82: abs (p - q) = r ; :: thesis:

per cases ;

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

hence contradiction by A61, A79, A82, ABSVALUE:def 1; :: thesis:

end;

suppose p - q < 0 ; :: thesis:

then abs (p - q) = - (p - q) by ABSVALUE:def 1;
hence contradiction by A61, A78, A82; :: thesis:

end;

hence y in Q by A39, A76, A77, A81, XXREAL_0:1; :: thesis:

end;

hence ( H is open & p in H & (Thunder G) .: H c= Q ) by A64, A66, A69, A70, TOPS_1:38, 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:48; :: thesis:

end;

hence Thunder G is continuous by TMAP_1:49; :: 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; :: thesis: