let X be non empty MetrSpace; :: thesis:
let Y be SetSequence of X; :: thesis:
assume that
A1: X is complete and
A2: union (rng Y) = the carrier of X and
A3: for n being Element of NAT holds (Y . n) ` in Family_open_set X ; :: thesis:
defpred S₁[ Element of NAT , Point of X, Real, Point of X, Real] means ( 0 < $3 & $3 < 1 / (2 |^ $1) & (Ball $2,$3) /\ (Y . $1) = {} implies ( 0 < $5 & $5 < 1 / (2 |^ ($1 + 1)) & Ball $4,$5 c= Ball $2,($3 / 2) & (Ball $4,$5) /\ (Y . ($1 + 1)) = {} ) );
assume A4: for n0 being Element of NAT
for r being Real
for x0 being Point of X holds
( not 0 < r or not Ball x0,r c= Y . n0 ) ; :: thesis:

consider x0 being Point of X;
A5: ( ((Y . 0 ) ` ) ` = the carrier of X \ ((Y . 0 ) ` ) & Ball x0,1 c= the carrier of X ) ;
assume (Y . 0 ) ` = {} ; :: thesis:
hence contradiction by A4, A5; :: thesis:

end;

then consider z0 being set such that
A6: z0 in (Y . 0 ) ` by XBOOLE_0:def 1;
reconsider z0 = z0 as Element of X by A6;
(Y . 0 ) ` in Family_open_set X by A3;
then consider t01 being Real such that
A7: 0 < t01 and
A8: Ball z0,t01 c= (Y . 0 ) ` by A6, PCOMPS_1:def 5;
reconsider t0 = min t01,(1 / 2) as Real ;
t0 <= 1 / 2 by XXREAL_0:17;
then t0 < 1 / 1 by XXREAL_0:2;
then A9: t0 < 1 / (2 |^ 0 ) by NEWTON:9;
Ball z0,t0 c= Ball z0,t01 by PCOMPS_1:1, XXREAL_0:17;
then Ball z0,t0 c= (Y . 0 ) ` by A8, XBOOLE_1:1;
then Ball z0,t0 misses Y . 0 by SUBSET_1:43;
then A10: (Ball z0,t0) /\ (Y . 0 ) = {} by XBOOLE_0:def 7;
A11: for n being Element of NAT
for x being Point of X
for r being Real ex x1 being Point of X ex r1 being Real st
( 0 < r & r < 1 / (2 |^ n) & (Ball x,r) /\ (Y . n) = {} implies ( 0 < r1 & r1 < 1 / (2 |^ (n + 1)) & Ball x1,r1 c= Ball x,(r / 2) & (Ball x1,r1) /\ (Y . (n + 1)) = {} ) )

proof

let n be Element of NAT ; :: thesis:
let x be Point of X; :: thesis:
let r be Real; :: thesis:

now

0 < 2 |^ (n + 2) by NEWTON:102;
then A12: 0 < 1 / (2 |^ (n + 2)) by XREAL_1:141;
0 < 2 |^ (n + 1) by NEWTON:102;
then A13: (1 / (2 |^ (n + 1))) / 2 < 1 / (2 |^ (n + 1)) by XREAL_1:141, XREAL_1:218;
2 |^ (n + 2) = 2 |^ ((n + 1) + 1)
.= (2 |^ (n + 1)) * 2 by NEWTON:11 ;
then A14: 1 / (2 |^ (n + 2)) = (1 / (2 |^ (n + 1))) / 2 by XCMPLX_1:79;
assume that
A15: 0 < r and
r < 1 / (2 |^ n) and
(Ball x,r) /\ (Y . n) = {} ; :: thesis:
not Ball x,(r / 2) c= Y . (n + 1) by A4, A15, XREAL_1:217;
then Ball x,(r / 2) meets (Y . (n + 1)) ` by SUBSET_1:44;
then consider z0 being set such that
A16: z0 in (Ball x,(r / 2)) /\ ((Y . (n + 1)) ` ) by XBOOLE_0:4;
reconsider x1 = z0 as Point of X by A16;
A17: (Y . (n + 1)) ` in Family_open_set X by A3;
( Ball x,(r / 2) in Family_open_set X & (Y . (n + 1)) ` in Family_open_set X ) by A3, PCOMPS_1:33;
then (Ball x,(r / 2)) /\ ((Y . (n + 1)) ` ) in Family_open_set X by PCOMPS_1:35;
then consider t02 being Real such that
A18: 0 < t02 and
A19: Ball x1,t02 c= (Ball x,(r / 2)) /\ ((Y . (n + 1)) ` ) by A16, PCOMPS_1:def 5;
A20: Ball x1,t02 c= Ball x,(r / 2) by A19, XBOOLE_1:18;
x1 in (Y . (n + 1)) ` by A16, XBOOLE_0:def 4;
then consider t01 being Real such that
A21: 0 < t01 and
A22: Ball x1,t01 c= (Y . (n + 1)) ` by A17, PCOMPS_1:def 5;
reconsider r1 = min (min t01,t02),(1 / (2 |^ (n + 2))) as Real ;
A23: r1 <= min t01,t02 by XXREAL_0:17;
min t01,t02 <= t02 by XXREAL_0:17;
then A24: Ball x1,r1 c= Ball x1,t02 by A23, PCOMPS_1:1, XXREAL_0:2;
min t01,t02 <= t01 by XXREAL_0:17;
then Ball x1,r1 c= Ball x1,t01 by A23, PCOMPS_1:1, XXREAL_0:2;
then Ball x1,r1 c= (Y . (n + 1)) ` by A22, XBOOLE_1:1;
then A25: Ball x1,r1 misses Y . (n + 1) by SUBSET_1:43;
take x1 = x1; :: thesis:
take r1 = r1; :: thesis:
A26: r1 <= 1 / (2 |^ (n + 2)) by XXREAL_0:17;
0 < min t01,t02 by A21, A18, XXREAL_0:15;
hence S₁[n,x,r,x1,r1] by A20, A14, A12, A13, A24, A25, A26, XBOOLE_0:def 7, XBOOLE_1:1, XXREAL_0:2, XXREAL_0:15; :: thesis:

end;

hence ex x1 being Point of X ex r1 being Real st
( 0 < r & r < 1 / (2 |^ n) & (Ball x,r) /\ (Y . n) = {} implies ( 0 < r1 & r1 < 1 / (2 |^ (n + 1)) & Ball x1,r1 c= Ball x,(r / 2) & (Ball x1,r1) /\ (Y . (n + 1)) = {} ) ) ; :: thesis:

end;

ex x0 being sequence of X ex r0 being Real_Sequence st
( x0 . 0 = z0 & r0 . 0 = t0 & ( for n being Element of NAT st 0 < r0 . n & r0 . n < 1 / (2 |^ n) & (Ball (x0 . n),(r0 . n)) /\ (Y . n) = {} holds
( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (x0 . (n + 1)),(r0 . (n + 1)) c= Ball (x0 . n),((r0 . n) / 2) & (Ball (x0 . (n + 1)),(r0 . (n + 1))) /\ (Y . (n + 1)) = {} ) ) )

proof

defpred S₂[ Element of NAT , Element of [:the carrier of X,REAL :], Element of [:the carrier of X,REAL :]] means ( 0 < $2 `2 & $2 `2 < 1 / (2 |^ $1) & (Ball ($2 `1 ),($2 `2 )) /\ (Y . $1) = {} implies ( 0 < $3 `2 & $3 `2 < 1 / (2 |^ ($1 + 1)) & Ball ($3 `1 ),($3 `2 ) c= Ball ($2 `1 ),(($2 `2 ) / 2) & (Ball ($3 `1 ),($3 `2 )) /\ (Y . ($1 + 1)) = {} ) );
A27: for n being Element of NAT
for u being Element of [:the carrier of X,REAL :] ex v being Element of [:the carrier of X,REAL :] st S₂[n,u,v]

proof

let n be Element of NAT ; :: thesis:
let u be Element of [:the carrier of X,REAL :]; :: thesis:
consider v1 being Element of X, v2 being Element of REAL such that
A28: S₁[n,u `1 ,u `2 ,v1,v2] by A11;
take [v1,v2] ; :: thesis:
[v1,v2] `1 = v1 by MCART_1:7;
hence S₂[n,u,[v1,v2]] by A28, MCART_1:7; :: thesis:

end;

consider f being Function of NAT ,[:the carrier of X,REAL :] such that
A29: ( f . 0 = [z0,t0] & ( for n being Element of NAT holds S₂[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A27);
take pr1 f ; :: thesis:
take pr2 f ; :: thesis:
thus (pr1 f) . 0 = (f . 0 ) `1 by FUNCT_2:def 6
.= z0 by A29, MCART_1:7 ; :: thesis:
thus (pr2 f) . 0 = (f . 0 ) `2 by FUNCT_2:def 7
.= t0 by A29, MCART_1:7 ; :: thesis:

hereby :: thesis:

let i be Element of NAT ; :: thesis:
A30: ( (f . (i + 1)) `1 = (pr1 f) . (i + 1) & (f . (i + 1)) `2 = (pr2 f) . (i + 1) ) by FUNCT_2:def 6, FUNCT_2:def 7;
( (f . i) `1 = (pr1 f) . i & (f . i) `2 = (pr2 f) . i ) by FUNCT_2:def 6, FUNCT_2:def 7;
hence S₁[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)] by A29, A30; :: thesis:

end;

then consider x0 being sequence of X, r0 being Real_Sequence such that
A31: ( x0 . 0 = z0 & r0 . 0 = t0 ) and
A32: for n being Element of NAT st 0 < r0 . n & r0 . n < 1 / (2 |^ n) & (Ball (x0 . n),(r0 . n)) /\ (Y . n) = {} holds
( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (x0 . (n + 1)),(r0 . (n + 1)) c= Ball (x0 . n),((r0 . n) / 2) & (Ball (x0 . (n + 1)),(r0 . (n + 1))) /\ (Y . (n + 1)) = {} ) ;
0 < 1 / 2 ;
then A33: 0 < t0 by A7, XXREAL_0:15;
A34: for n being Element of NAT holds
( 0 < r0 . n & r0 . n < 1 / (2 |^ n) & Ball (x0 . (n + 1)),(r0 . (n + 1)) c= Ball (x0 . n),((r0 . n) / 2) & (Ball (x0 . n),(r0 . n)) /\ (Y . n) = {} )

proof

defpred S₂[ Element of NAT ] means ( 0 < r0 . $1 & r0 . $1 < 1 / (2 |^ $1) & Ball (x0 . ($1 + 1)),(r0 . ($1 + 1)) c= Ball (x0 . $1),((r0 . $1) / 2) & (Ball (x0 . $1),(r0 . $1)) /\ (Y . $1) = {} );

A35: now

let n be Element of NAT ; :: thesis:
assume A36: S₂[n] ; :: thesis:
then A37: (Ball (x0 . (n + 1)),(r0 . (n + 1))) /\ (Y . (n + 1)) = {} by A32;
( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) ) by A32, A36;
hence S₂[n + 1] by A32, A37; :: thesis:

end;

A38: S₂[ 0 ] by A33, A9, A10, A31, A32;
thus for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A38, A35); :: thesis:

end;

A39: for m, k being Element of NAT holds dist (x0 . (m + k)),(x0 . m) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))

proof

let m be Element of NAT ; :: thesis:
defpred S₂[ Element of NAT ] means dist (x0 . (m + $1)),(x0 . m) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ $1)));

A40: now

let k be Element of NAT ; :: thesis:
assume S₂[k] ; :: thesis:
then A41: (dist (x0 . ((m + k) + 1)),(x0 . (m + k))) + (dist (x0 . (m + k)),(x0 . m)) <= (dist (x0 . ((m + k) + 1)),(x0 . (m + k))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by XREAL_1:8;
( 0 < r0 . ((m + k) + 1) & dist (x0 . ((m + k) + 1)),(x0 . ((m + k) + 1)) = 0 ) by A34, METRIC_1:1;
then A42: x0 . ((m + k) + 1) in Ball (x0 . ((m + k) + 1)),(r0 . ((m + k) + 1)) by METRIC_1:12;
r0 . (m + k) < 1 / (2 |^ (m + k)) by A34;
then (r0 . (m + k)) / 2 < (1 / (2 |^ (m + k))) / 2 by XREAL_1:76;
then (r0 . (m + k)) / 2 < 1 / ((2 |^ (m + k)) * 2) by XCMPLX_1:79;
then A43: (r0 . (m + k)) / 2 < 1 / (2 |^ ((m + k) + 1)) by NEWTON:11;
Ball (x0 . ((m + k) + 1)),(r0 . ((m + k) + 1)) c= Ball (x0 . (m + k)),((r0 . (m + k)) / 2) by A34;
then dist (x0 . ((m + k) + 1)),(x0 . (m + k)) < (r0 . (m + k)) / 2 by A42, METRIC_1:12;
then dist (x0 . ((m + k) + 1)),(x0 . (m + k)) <= 1 / (2 |^ ((m + k) + 1)) by A43, XXREAL_0:2;
then A44: (dist (x0 . ((m + k) + 1)),(x0 . (m + k))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) <= (1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by XREAL_1:8;
2 |^ (m + (k + 1)) = (2 |^ m) * (2 |^ (k + 1)) by NEWTON:13;
then 1 / (2 |^ ((m + k) + 1)) = (1 / (2 |^ m)) / ((2 |^ (k + 1)) / 1) by XCMPLX_1:79
.= (1 / (2 |^ m)) * (1 / (2 |^ (k + 1))) by XCMPLX_1:80 ;
then A45: (1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) = (1 / (2 |^ m)) * (1 + ((1 / (2 |^ (k + 1))) - (1 / (2 |^ k))))
.= (1 / (2 |^ m)) * (1 + ((1 / ((2 |^ k) * 2)) - (1 / (2 |^ k)))) by NEWTON:11
.= (1 / (2 |^ m)) * (1 + (((1 / (2 |^ k)) / 2) - (1 / (2 |^ k)))) by XCMPLX_1:79
.= (1 / (2 |^ m)) * (1 - ((1 / (2 |^ k)) / 2))
.= (1 / (2 |^ m)) * (1 - (1 / ((2 |^ k) * 2))) by XCMPLX_1:79 ;
dist (x0 . ((m + k) + 1)),(x0 . m) <= (dist (x0 . ((m + k) + 1)),(x0 . (m + k))) + (dist (x0 . (m + k)),(x0 . m)) by METRIC_1:4;
then dist (x0 . (m + (k + 1))),(x0 . m) <= (dist (x0 . ((m + k) + 1)),(x0 . (m + k))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by A41, XXREAL_0:2;
then dist (x0 . (m + (k + 1))),(x0 . m) <= (1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by A44, XXREAL_0:2;
hence S₂[k + 1] by A45, NEWTON:11; :: thesis:

end;

2 |^ 0 = 1 by NEWTON:9;
then A46: S₂[ 0 ] by METRIC_1:1;
for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A46, A40);
hence for k being Element of NAT holds dist (x0 . (m + k)),(x0 . m) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) ; :: thesis:

end;

A47: now

let m be Element of NAT ; :: thesis:

hereby :: thesis:

end;

now

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider p1 being Element of NAT such that
A50: 1 / (2 |^ p1) <= r by PREPOWER:106;
take p = p1 + 1; :: thesis:

hereby :: thesis:

let n, m be Element of NAT ; :: thesis:
assume that
A51: n >= p and
A52: m >= p ; :: thesis:
consider k1 being Nat such that
A53: n = p + k1 by A51, NAT_1:10;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
n = p + k1 by A53;
then A54: dist (x0 . n),(x0 . p) < 1 / (2 |^ p) by A47;
consider k2 being Nat such that
A55: m = p + k2 by A52, NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 13;
A56: 1 / (2 |^ p) = 1 / ((2 |^ p1) * 2) by NEWTON:11
.= (1 / (2 |^ p1)) / 2 by XCMPLX_1:79 ;
m = p + k2 by A55;
then A57: (dist (x0 . n),(x0 . p)) + (dist (x0 . p),(x0 . m)) < (1 / (2 |^ p)) + (1 / (2 |^ p)) by A47, A54, XREAL_1:10;
dist (x0 . n),(x0 . m) <= (dist (x0 . n),(x0 . p)) + (dist (x0 . p),(x0 . m)) by METRIC_1:4;
then dist (x0 . n),(x0 . m) < 1 / (2 |^ p1) by A57, A56, XXREAL_0:2;
hence dist (x0 . n),(x0 . m) < r by A50, XXREAL_0:2; :: thesis:

end;

then x0 is Cauchy by TBSP_1:def 5;
then A58: x0 is convergent by A1, TBSP_1:def 6;
A59: for m, k being Element of NAT holds Ball (x0 . ((m + 1) + k)),(r0 . ((m + 1) + k)) c= Ball (x0 . m),((r0 . m) / 2)

proof

let m be Element of NAT ; :: thesis:
defpred S₂[ Element of NAT ] means Ball (x0 . ((m + 1) + $1)),(r0 . ((m + 1) + $1)) c= Ball (x0 . m),((r0 . m) / 2);

A60: now

let k be Element of NAT ; :: thesis:
assume A61: S₂[k] ; :: thesis:
0 < r0 . ((m + 1) + k) by A34;
then (r0 . ((m + 1) + k)) / 2 < r0 . ((m + 1) + k) by XREAL_1:218;
then A62: Ball (x0 . ((m + 1) + k)),((r0 . ((m + 1) + k)) / 2) c= Ball (x0 . ((m + 1) + k)),(r0 . ((m + 1) + k)) by PCOMPS_1:1;
Ball (x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1))) = Ball (x0 . (((m + 1) + k) + 1)),(r0 . (((m + 1) + k) + 1)) ;
then Ball (x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1))) c= Ball (x0 . ((m + 1) + k)),((r0 . ((m + 1) + k)) / 2) by A34;
then Ball (x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1))) c= Ball (x0 . ((m + 1) + k)),(r0 . ((m + 1) + k)) by A62, XBOOLE_1:1;
hence S₂[k + 1] by A61, XBOOLE_1:1; :: thesis:

end;

A63: S₂[ 0 ] by A34;
thus for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A63, A60); :: thesis:

end;

A64: now

let m be Element of NAT ; :: thesis:
set m1 = m + 1;
0 < r0 . m by A34;
then 0 < (r0 . m) / 2 by XREAL_1:217;
then consider n1 being Element of NAT such that
A65: for l being Element of NAT st n1 <= l holds
dist (x0 . l),(lim x0) < (r0 . m) / 2 by A58, TBSP_1:def 4;
reconsider n = max n1,(m + 1) as Element of NAT by XXREAL_0:16;
A66: dist (x0 . n),(lim x0) < (r0 . m) / 2 by A65, XXREAL_0:25;
consider k being Nat such that
A67: n = (m + 1) + k by NAT_1:10, XXREAL_0:25;
( dist (x0 . n),(x0 . n) = 0 & 0 < r0 . n ) by A34, METRIC_1:1;
then A68: x0 . n in Ball (x0 . n),(r0 . n) by METRIC_1:12;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
n = (m + 1) + k by A67;
then Ball (x0 . n),(r0 . n) c= Ball (x0 . m),((r0 . m) / 2) by A59;
then dist (x0 . n),(x0 . m) < (r0 . m) / 2 by A68, METRIC_1:12;
then A69: (dist (lim x0),(x0 . n)) + (dist (x0 . n),(x0 . m)) < ((r0 . m) / 2) + ((r0 . m) / 2) by A66, XREAL_1:10;
dist (lim x0),(x0 . m) <= (dist (lim x0),(x0 . n)) + (dist (x0 . n),(x0 . m)) by METRIC_1:4;
then dist (lim x0),(x0 . m) < ((r0 . m) / 2) + ((r0 . m) / 2) by A69, XXREAL_0:2;
hence lim x0 in Ball (x0 . m),(r0 . m) by METRIC_1:12; :: thesis:

end;

A70: now

let n be Element of NAT ; :: thesis:
thus not lim x0 in Y . n :: thesis:

proof

assume A71: lim x0 in Y . n ; :: thesis:
lim x0 in Ball (x0 . n),(r0 . n) by A64;
then lim x0 in (Ball (x0 . n),(r0 . n)) /\ (Y . n) by A71, XBOOLE_0:def 4;
hence contradiction by A34; :: thesis:

end;

not lim x0 in union (rng Y)

proof

assume lim x0 in union (rng Y) ; :: thesis:
then consider A being set such that
A72: lim x0 in A and
A73: A in rng Y by TARSKI:def 4;
ex k being set st
( k in dom Y & A = Y . k ) by A73, FUNCT_1:def 5;
hence contradiction by A70, A72; :: thesis:

end;

hence contradiction by A2; :: thesis: