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 S_{1}[ 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)) & S_{1}[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 S_{2}[ 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 S_{3}[ Nat, Element of D, Element of D] means S_{2}[$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 S_{3}[n,x,y]

( F . 0 = S & ( for n being Nat holds S_{3}[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 S_{2}[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 S_{4}[ 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 S_{5}[ 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 S_{5}[n] holds

S_{5}[n + 1]

( 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 S_{4}[ 0 ,xx,yy]
by A33;

then A37: S_{5}[ 0 ]
by A32;

for n being Nat holds S_{5}[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

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 S

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)) & S

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 S

( 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 S

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 S

proof

ex F being sequence of D st
let n be Nat; :: thesis: for x being Element of D ex y being Element of D st S_{3}[n,x,y]

let x be Element of D; :: thesis: ex y being Element of D st S_{3}[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

yy is Drizzle of A,B,k + 1

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 S_{2}[x,y]

A31: S_{2}[x,y]
;

take y ; :: thesis: S_{3}[n,x,y]

thus S_{3}[n,x,y]
by A31; :: thesis: verum

end;let x be Element of D; :: thesis: ex y being Element of D st S

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

A9:
for k being Nat st xx is Drizzle of A,B,k holds
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;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

yy is Drizzle of A,B,k + 1

proof

reconsider xx = xx as Element of PFuncs (DYADIC,(bool the carrier of T)) by Th3;
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

end;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

hence
yy is Drizzle of A,B,k + 1
; :: thesis: verum
assume A11:
k <> s0
; :: thesis: contradiction

end;per cases
( k < s0 or s0 < k )
by A11, XXREAL_0:1;

end;

suppose A12:
k < s0
; :: thesis: contradiction

set o = 1 / (2 |^ s0);

A13: not 1 / (2 |^ s0) in dyadic k

then 1 / (2 |^ s0) in dyadic s0 by URYSOHN1:def 1;

hence contradiction by A10, A13, FUNCT_2:def 1; :: thesis: verum

end;A13: not 1 / (2 |^ s0) in dyadic k

proof

1 <= 2 |^ s0
by PREPOWER:11;
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

hence contradiction by A19, NAT_1:6; :: thesis: verum

end;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

i <> 0
by A17, NEWTON:83;
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;(n + 1) - 1 < 0 by A18, A14, A20, XREAL_1:49, XREAL_1:83;

hence contradiction ; :: thesis: verum

hence contradiction by A19, NAT_1:6; :: thesis: verum

then 1 / (2 |^ s0) in dyadic s0 by URYSOHN1:def 1;

hence contradiction by A10, A13, FUNCT_2:def 1; :: thesis: verum

suppose A21:
s0 < k
; :: thesis: contradiction

set o = 1 / (2 |^ k);

A22: not 1 / (2 |^ k) in dyadic s0

then 1 / (2 |^ k) in dyadic k by URYSOHN1:def 1;

hence contradiction by A10, A22, FUNCT_2:def 1; :: thesis: verum

end;A22: not 1 / (2 |^ k) in dyadic s0

proof

1 <= 2 |^ k
by PREPOWER:11;
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

hence contradiction by A28, NAT_1:6; :: thesis: verum

end;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

i <> 0
by A26, NEWTON:83;
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;(n + 1) - 1 < 0 by A27, A23, A29, XREAL_1:49, XREAL_1:83;

hence contradiction ; :: thesis: verum

hence contradiction by A28, NAT_1:6; :: thesis: verum

then 1 / (2 |^ k) in dyadic k by URYSOHN1:def 1;

hence contradiction by A10, A22, FUNCT_2:def 1; :: thesis: verum

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 S

proof

then consider y being Element of D such that
take
yy
; :: thesis: S_{2}[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;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

A31: S

take y ; :: thesis: S

thus S

( F . 0 = S & ( for n being Nat holds S

then consider F being sequence of D such that

A32: F . 0 = S and

A33: for n being Nat holds S

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 S

$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 S

A35: for n being Nat st S

S

proof

take
F
; :: thesis: for n being Nat holds
let n be Nat; :: thesis: ( S_{5}[n] implies S_{5}[n + 1] )

assume A36: S_{5}[n]
; :: thesis: S_{5}[n + 1]

ex xx, yy being PartFunc of DYADIC,(bool the carrier of T) st S_{4}[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 S_{4}[n + 1,xx1,yy1]
by A33;

hence (F . (n + 1)) . r = (F . ((n + 1) + 1)) . r ; :: thesis: verum

end;assume A36: S

ex xx, yy being PartFunc of DYADIC,(bool the carrier of T) st S

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 S

hence (F . (n + 1)) . r = (F . ((n + 1) + 1)) . r ; :: thesis: verum

( 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 S

then A37: S

for n being Nat holds S

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