let T be non empty normal TopSpace; :: thesis:
let A, B be closed Subset of T; :: thesis:
assume A1: ( A <> {} & A misses B ) ; :: thesis:
defpred S₁[ set ] means ex n being Element of NAT st $1 is Drizzle of A,B,n;
consider D being set such that
A2: for x being set holds
( x in D iff ( x in PFuncs DYADIC ,(bool the carrier of T) & S₁[x] ) ) from XBOOLE_0:sch 1();
consider S being Drizzle of A,B, 0 ;
A3: S is Element of PFuncs DYADIC ,(bool the carrier of T) by Th4;
then reconsider D = D as non empty set by A2;
reconsider S = S as Element of D by A2, A3;
defpred S₂[ Element of D, Element of D] means ex xx, yy being PartFunc of DYADIC ,(bool the carrier of T) st
( xx = $1 & yy = $2 & ex k being Element of NAT st xx is Drizzle of A,B,k & ( for k being Element of NAT st xx is Drizzle of A,B,k holds
yy is Drizzle of A,B,k + 1 ) & ( for r being Element of dom xx holds xx . r = yy . r ) );
defpred S₃[ Element of NAT , Element of D, Element of D] means S₂[$2,$3];
A4: for n being Element of NAT
for x being Element of D ex y being Element of D st S₃[n,x,y]

let n be Element of NAT ; :: thesis:
let x be Element of D; :: thesis:
consider s0 being Element of NAT such that
A5: x is Drizzle of A,B,s0 by A2;
reconsider xx = x as Drizzle of A,B,s0 by A5;
consider yy being Drizzle of A,B,s0 + 1 such that
A6: for r being Element of dyadic (s0 + 1) st r in dyadic s0 holds
yy . r = xx . r by A1, Th3;
A7: for k being Element of NAT st xx is Drizzle of A,B,k holds
yy is Drizzle of A,B,k + 1

let k be Element of NAT ; :: thesis:
assume xx is Drizzle of A,B,k ; :: thesis:
then A8: dom xx = dyadic k by FUNCT_2:def 1;
k = s0

assume A9: k <> s0 ; :: thesis:

per cases by A9, XXREAL_0:1;

suppose A10: k < s0 ; :: thesis:

set o = 1 / (2 |^ s0);
( 0 <= 1 & 1 <= 2 |^ s0 & 1 / (2 |^ s0) = 1 / (2 |^ s0) ) by PREPOWER:19;
then A11: 1 / (2 |^ s0) in dyadic s0 by URYSOHN1:def 3;
not 1 / (2 |^ s0) in dyadic k

assume 1 / (2 |^ s0) in dyadic k ; :: thesis:
then consider i being Element of NAT such that
A12: ( 0 <= i & i <= 2 |^ k & 1 / (2 |^ s0) = i / (2 |^ k) ) by URYSOHN1:def 3;
A13: ( 0 < 2 |^ s0 & 0 < 2 |^ k ) by NEWTON:102;
then A14: 1 * (2 |^ k) = i * (2 |^ s0) by A12, XCMPLX_1:96;
then A15: i = (2 |^ k) / (2 |^ s0) by A13, XCMPLX_1:90;
A16: i <> 0 by A14, NEWTON:102;
2 |^ k < 1 * (2 |^ s0) by A10, PEPIN:71;
then A17: i < 1 by A15, XREAL_1:85;
for n being Nat holds not i = n + 1

given n being Nat such that A18: i = n + 1 ; :: thesis:
(n + 1) - 1 < 0 by A17, A18, XREAL_1:51;
hence contradiction ; :: thesis:

end;

hence contradiction by A16, NAT_1:6; :: thesis:

end;

hence contradiction by A8, A11, FUNCT_2:def 1; :: thesis:

end;

suppose A19: s0 < k ; :: thesis:

set o = 1 / (2 |^ k);
( 0 <= 1 & 1 <= 2 |^ k & 1 / (2 |^ k) = 1 / (2 |^ k) ) by PREPOWER:19;
then A20: 1 / (2 |^ k) in dyadic k by URYSOHN1:def 3;
not 1 / (2 |^ k) in dyadic s0

assume 1 / (2 |^ k) in dyadic s0 ; :: thesis:
then consider i being Element of NAT such that
A21: ( 0 <= i & i <= 2 |^ s0 & 1 / (2 |^ k) = i / (2 |^ s0) ) by URYSOHN1:def 3;
A22: ( 0 < 2 |^ s0 & 0 < 2 |^ k ) by NEWTON:102;
then A23: 1 * (2 |^ s0) = i * (2 |^ k) by A21, XCMPLX_1:96;
then A24: i = (2 |^ s0) / (2 |^ k) by A22, XCMPLX_1:90;
A25: i <> 0 by A23, NEWTON:102;
2 |^ s0 < 1 * (2 |^ k) by A19, PEPIN:71;
then A26: i < 1 by A24, XREAL_1:85;
for n being Nat holds not i = n + 1

given n being Nat such that A27: i = n + 1 ; :: thesis:
(n + 1) - 1 < 0 by A26, A27, XREAL_1:51;
hence contradiction ; :: thesis:

end;

hence contradiction by A25, NAT_1:6; :: thesis:

end;

hence contradiction by A8, A20, FUNCT_2:def 1; :: thesis:

end;

hence yy is Drizzle of A,B,k + 1 ; :: thesis:

end;

A28: for r being Element of dom xx holds xx . r = yy . r

let r be Element of dom xx; :: thesis:
dom xx = dyadic s0 by FUNCT_2:def 1;
then A29: r in dyadic s0 ;
dyadic s0 c= dyadic (s0 + 1) by URYSOHN1:11;
hence xx . r = yy . r by A6, A29; :: thesis:

end;

reconsider xx = xx as Element of PFuncs DYADIC ,(bool the carrier of T) by Th4;
reconsider xx = xx as Element of D ;
A30: yy is Element of PFuncs DYADIC ,(bool the carrier of T) by Th4;
then reconsider yy = yy as Element of D by A2;
ex y being Element of D st S₂[x,y]

take yy ; :: thesis:
reconsider xx = xx as PartFunc of DYADIC ,(bool the carrier of T) by PARTFUN1:121;
reconsider yy = yy as PartFunc of DYADIC ,(bool the carrier of T) by A30, PARTFUN1:120;
take xx ; :: thesis:
take yy ; :: thesis:
thus ( xx = x & yy = yy & ex k being Element of NAT st xx is Drizzle of A,B,k & ( for k being Element of NAT st xx is Drizzle of A,B,k holds
yy is Drizzle of A,B,k + 1 ) & ( for r being Element of dom xx holds xx . r = yy . r ) ) by A7, A28; :: thesis:

end;

then consider y being Element of D such that
A31: S₂[x,y] ;
take y ; :: thesis:
thus S₃[n,x,y] by A31; :: thesis:

end;

ex F being Function of NAT ,D st
( F . 0 = S & ( for n being Element of NAT holds S₃[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A4);
then consider F being Function of NAT ,D such that
A32: ( F . 0 = S & ( for n being Element of NAT holds S₂[F . n,F . (n + 1)] ) ) ;
defpred S₄[ Element of NAT , PartFunc of DYADIC ,(bool the carrier of T), PartFunc of DYADIC ,(bool the carrier of T)] means ( $2 = F . $1 & $3 = F . ($1 + 1) & ex k being Element of NAT st $2 is Drizzle of A,B,k & ( for k being Element of NAT st $2 is Drizzle of A,B,k holds
$3 is Drizzle of A,B,k + 1 ) & ( for r being Element of dom $2 holds $2 . r = $3 . r ) );
A33: ( F is Function & dom F = NAT & rng F c= D ) by FUNCT_2:def 1, RELAT_1:def 19;
for x being set st x in D holds
x in PFuncs DYADIC ,(bool the carrier of T) by A2;
then D c= PFuncs DYADIC ,(bool the carrier of T) by TARSKI:def 3;
then ( F is Function & dom F = NAT & rng F c= PFuncs DYADIC ,(bool the carrier of T) ) by A33, XBOOLE_1:1;
then reconsider F = F as Functional_Sequence of DYADIC ,(bool the carrier of T) by FUNCT_2:def 1, RELSET_1:11;
defpred S₅[ Element of NAT ] means ( F . $1 is Drizzle of A,B,$1 & ( for r being Element of dom (F . $1) holds (F . $1) . r = (F . ($1 + 1)) . r ) );
ex xx, yy being PartFunc of DYADIC ,(bool the carrier of T) st S₄[ 0 ,xx,yy] by A32;
then A34: S₅[ 0 ] by A32;
A35: for n being Element of NAT st S₅[n] holds
S₅[n + 1]

let n be Element of NAT ; :: thesis:
assume A36: S₅[n] ; :: thesis:
consider xx, yy being PartFunc of DYADIC ,(bool the carrier of T) such that
A37: S₄[n,xx,yy] by A32;
thus F . (n + 1) is Drizzle of A,B,n + 1 by A36, A37; :: thesis:
let r be Element of dom (F . (n + 1)); :: thesis:
consider xx1, yy1 being PartFunc of DYADIC ,(bool the carrier of T) such that
A38: S₄[n + 1,xx1,yy1] by A32;
thus (F . (n + 1)) . r = (F . ((n + 1) + 1)) . r by A38; :: thesis:

end;

A39: for n being Element of NAT holds S₅[n] from NAT_1:sch 1(A34, A35);
take F ; :: thesis:
thus for n being Element of NAT holds
( F . n is Drizzle of A,B,n & ( for r being Element of dom (F . n) holds (F . n) . r = (F . (n + 1)) . r ) ) by A39; :: thesis: