let T be non empty normal TopSpace; :: thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
ex F being Functional_Sequence of DYADIC,(bool the carrier of T) st
for n being 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 ) )
let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies ex F being Functional_Sequence of DYADIC,(bool the carrier of T) st
for n being 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 ) ) )
defpred S1[ object ] means ex n being Nat st $1 is Drizzle of A,B,n;
consider D being set such that
A1: for x being object holds
( x in D iff ( x in PFuncs (DYADIC,(bool the carrier of T)) & S1[x] ) ) from XBOOLE_0:sch 1();
 set S = the Drizzle of A,B, 0 ;
A2: the Drizzle of A,B, 0 is Element of PFuncs (DYADIC,(bool the carrier of T)) by Th3;
then reconsider D = D as non empty set by A1;
reconsider S = the Drizzle of A,B, 0 as Element of D by A1, A2;
defpred S2[ 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 Nat st xx is Drizzle of A,B,k & ( for k being 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 S3[ Nat, Element of D, Element of D] means S2[$2,$3];
assume A3: ( A <> {} & A misses B ) ; :: thesis: ex F being Functional_Sequence of DYADIC,(bool the carrier of T) st
for n being 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 ) )
A4: for n being Nat
for x being Element of D ex y being Element of D st S3[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of D ex y being Element of D st S3[n,x,y]
let x be Element of D; :: thesis: ex y being Element of D st S3[n,x,y]
consider s0 being Nat such that
A5: x is Drizzle of A,B,s0 by A1;
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 A3, Th2;
A7: for r being Element of dom xx holds xx . r = yy . r
proof
let r be Element of dom xx; :: thesis: xx . r = yy . r
dom xx = dyadic s0 by FUNCT_2:def 1;
then A8: r in dyadic s0 ;
dyadic s0 c= dyadic (s0 + 1) by URYSOHN1:5;
hence xx . r = yy . r by A6, A8; :: thesis: verum
end;
A9: for k being Nat st xx is Drizzle of A,B,k holds
yy is Drizzle of A,B,k + 1
proof
let k be Nat; :: thesis: ( xx is Drizzle of A,B,k implies yy is Drizzle of A,B,k + 1 )
assume xx is Drizzle of A,B,k ; :: thesis: yy is Drizzle of A,B,k + 1
then A10: dom xx = dyadic k by FUNCT_2:def 1;
k = s0
proof
assume A11: k <> s0 ; :: thesis: contradiction
per cases ( k < s0 or s0 < k ) by A11, XXREAL_0:1;
suppose A12: k < s0 ; :: thesis: contradiction
set o = 1 / (2 |^ s0);
A13: not 1 / (2 |^ s0) in dyadic k
proof
A14: 2 |^ k < 1 * (2 |^ s0) by A12, PEPIN:66;
assume 1 / (2 |^ s0) in dyadic k ; :: thesis: contradiction
then consider i being Nat such that
i <= 2 |^ k and
A15: 1 / (2 |^ s0) = i / (2 |^ k) by URYSOHN1:def 1;
A16: 0 < 2 |^ s0 by NEWTON:83;
0 < 2 |^ k by NEWTON:83;
then A17: 1 * (2 |^ k) = i * (2 |^ s0) by A15, A16, XCMPLX_1:95;
then A18: i = (2 |^ k) / (2 |^ s0) by A16, XCMPLX_1:89;
A19: for n being Nat holds not i = n + 1
proof
given n being Nat such that A20: i = n + 1 ; :: thesis: contradiction
(n + 1) - 1 < 0 by A18, A14, A20, XREAL_1:49, XREAL_1:83;
hence contradiction ; :: thesis: verum
end;
i <> 0 by A17, NEWTON:83;
hence contradiction by A19, NAT_1:6; :: thesis: verum
end;
1 <= 2 |^ s0 by PREPOWER:11;
then 1 / (2 |^ s0) in dyadic s0 by URYSOHN1:def 1;
hence contradiction by A10, A13, FUNCT_2:def 1; :: thesis: verum
end;
suppose A21: s0 < k ; :: thesis: contradiction
set o = 1 / (2 |^ k);
A22: not 1 / (2 |^ k) in dyadic s0
proof
A23: 2 |^ s0 < 1 * (2 |^ k) by A21, PEPIN:66;
assume 1 / (2 |^ k) in dyadic s0 ; :: thesis: contradiction
then consider i being Nat such that
i <= 2 |^ s0 and
A24: 1 / (2 |^ k) = i / (2 |^ s0) by URYSOHN1:def 1;
A25: 0 < 2 |^ k by NEWTON:83;
0 < 2 |^ s0 by NEWTON:83;
then A26: 1 * (2 |^ s0) = i * (2 |^ k) by A24, A25, XCMPLX_1:95;
then A27: i = (2 |^ s0) / (2 |^ k) by A25, XCMPLX_1:89;
A28: for n being Nat holds not i = n + 1
proof
given n being Nat such that A29: i = n + 1 ; :: thesis: contradiction
(n + 1) - 1 < 0 by A27, A23, A29, XREAL_1:49, XREAL_1:83;
hence contradiction ; :: thesis: verum
end;
i <> 0 by A26, NEWTON:83;
hence contradiction by A28, NAT_1:6; :: thesis: verum
end;
1 <= 2 |^ k by PREPOWER:11;
then 1 / (2 |^ k) in dyadic k by URYSOHN1:def 1;
hence contradiction by A10, A22, FUNCT_2:def 1; :: thesis: verum
end;
end;
end;
hence yy is Drizzle of A,B,k + 1 ; :: thesis: verum
end;
reconsider xx = xx as Element of PFuncs (DYADIC,(bool the carrier of T)) by Th3;
reconsider xx = xx as Element of D ;
A30: yy is Element of PFuncs (DYADIC,(bool the carrier of T)) by Th3;
then reconsider yy = yy as Element of D by A1;
ex y being Element of D st S2[x,y]
proof
take yy ; :: thesis: S2[x,yy]
reconsider yy = yy as PartFunc of DYADIC,(bool the carrier of T) by A30, PARTFUN1:46;
reconsider xx = xx as PartFunc of DYADIC,(bool the carrier of T) by PARTFUN1:47;
take xx ; :: thesis: ex yy being PartFunc of DYADIC,(bool the carrier of T) st
( xx = x & yy = yy & ex k being Nat st xx is Drizzle of A,B,k & ( for k being 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 ) )
take yy ; :: thesis: ( xx = x & yy = yy & ex k being Nat st xx is Drizzle of A,B,k & ( for k being 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 ) )
thus ( xx = x & yy = yy & ex k being Nat st xx is Drizzle of A,B,k & ( for k being 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 A9, A7; :: thesis: verum
end;
then consider y being Element of D such that
A31: S2[x,y] ;
take y ; :: thesis: S3[n,x,y]
thus S3[n,x,y] by A31; :: thesis: verum
end;
ex F being sequence of D st
( F . 0 = S & ( for n being Nat holds S3[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A4);
 then consider F being sequence of D such that
A32: F . 0 = S and
A33: for n being Nat holds S2[F . n,F . (n + 1)] ;
for x being object st x in D holds
x in PFuncs (DYADIC,(bool the carrier of T)) by A1;
then ( rng F c= D & D c= PFuncs (DYADIC,(bool the carrier of T)) ) by RELAT_1:def 19;
then A34: ( dom F = NAT & rng F c= PFuncs (DYADIC,(bool the carrier of T)) ) by FUNCT_2:def 1;
defpred S4[ 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 Nat st $2 is Drizzle of A,B,k & ( for k being 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 ) );
reconsider F = F as Functional_Sequence of DYADIC,(bool the carrier of T) by A34, FUNCT_2:def 1, RELSET_1:4;
defpred S5[ 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 ) );
A35: for n being Nat st S5[n] holds
S5[n + 1]
proof
let n be Nat; :: thesis: ( S5[n] implies S5[n + 1] )
assume A36: S5[n] ; :: thesis: S5[n + 1]
ex xx, yy being PartFunc of DYADIC,(bool the carrier of T) st S4[n,xx,yy] by A33;
hence F . (n + 1) is Drizzle of A,B,n + 1 by A36; :: thesis: for r being Element of dom (F . (n + 1)) holds (F . (n + 1)) . r = (F . ((n + 1) + 1)) . r
let r be Element of dom (F . (n + 1)); :: thesis: (F . (n + 1)) . r = (F . ((n + 1) + 1)) . r
ex xx1, yy1 being PartFunc of DYADIC,(bool the carrier of T) st S4[n + 1,xx1,yy1] by A33;
hence (F . (n + 1)) . r = (F . ((n + 1) + 1)) . r ; :: thesis: verum
end;
take F ; :: thesis: for n being 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 ) )
ex xx, yy being PartFunc of DYADIC,(bool the carrier of T) st S4[ 0 ,xx,yy] by A33;
then A37: S5[ 0 ] by A32;
for n being Nat holds S5[n] from NAT_1:sch 2(A37, A35);
 hence for n being 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 ) ) ; :: thesis: verum