let X be non empty MetrSpace; :: thesis: for Y being SetSequence of X st X is complete & union (rng Y) = the carrier of X & ( for n being Nat holds (Y . n) ` in Family_open_set X ) holds

ex n0 being Nat ex r being Real ex x0 being Point of X st

( 0 < r & Ball (x0,r) c= Y . n0 )

let Y be SetSequence of X; :: thesis: ( X is complete & union (rng Y) = the carrier of X & ( for n being Nat holds (Y . n) ` in Family_open_set X ) implies ex n0 being Nat ex r being Real ex x0 being Point of X st

( 0 < r & Ball (x0,r) c= Y . n0 ) )

assume that

A1: X is complete and

A2: union (rng Y) = the carrier of X and

A3: for n being Nat holds (Y . n) ` in Family_open_set X ; :: thesis: ex n0 being Nat ex r being Real ex x0 being Point of X st

( 0 < r & Ball (x0,r) c= Y . n0 )

defpred S_{1}[ 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 Nat

for r being Real

for x0 being Point of X holds

( not 0 < r or not Ball (x0,r) c= Y . n0 ) ; :: thesis: contradiction

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

reconsider t0 = min (t01,(1 / 2)) as Element of REAL by XREAL_0:def 1;

t0 <= 1 / 2 by XXREAL_0:17;

then t0 < 1 / 1 by XXREAL_0:2;

then A9: t0 < 1 / (2 |^ 0) by NEWTON:4;

Ball (z0,t0) c= Ball (z0,t01) by PCOMPS_1:1, XXREAL_0:17;

then Ball (z0,t0) c= (Y . 0) ` by A8;

then Ball (z0,t0) misses Y . 0 by SUBSET_1:23;

then A10: (Ball (z0,t0)) /\ (Y . 0) = {} by XBOOLE_0:def 7;

A11: for n being 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)) = {} ) )

( x0 . 0 = z0 & r0 . 0 = t0 & ( for n being 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)) = {} ) ) )

A32: ( x0 . 0 = z0 & r0 . 0 = t0 ) and

A33: for n being 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 A34: 0 < t0 by A7, XXREAL_0:15;

A35: for n being 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) = {} )

then A59: x0 is convergent by A1, TBSP_1:def 5;

A60: for m, k being Nat holds Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) c= Ball ((x0 . m),((r0 . m) / 2))

ex n0 being Nat ex r being Real ex x0 being Point of X st

( 0 < r & Ball (x0,r) c= Y . n0 )

let Y be SetSequence of X; :: thesis: ( X is complete & union (rng Y) = the carrier of X & ( for n being Nat holds (Y . n) ` in Family_open_set X ) implies ex n0 being Nat ex r being Real ex x0 being Point of X st

( 0 < r & Ball (x0,r) c= Y . n0 ) )

assume that

A1: X is complete and

A2: union (rng Y) = the carrier of X and

A3: for n being Nat holds (Y . n) ` in Family_open_set X ; :: thesis: ex n0 being Nat ex r being Real ex x0 being Point of X st

( 0 < r & Ball (x0,r) c= Y . n0 )

defpred S

assume A4: for n0 being Nat

for r being Real

for x0 being Point of X holds

( not 0 < r or not Ball (x0,r) c= Y . n0 ) ; :: thesis: contradiction

now :: thesis: not (Y . 0) ` = {}

then consider z0 being object such that set x0 = the Point of X;

A5: ( ((Y . 0) `) ` = the carrier of X \ ((Y . 0) `) & Ball ( the Point of X,1) c= the carrier of X ) ;

assume (Y . 0) ` = {} ; :: thesis: contradiction

hence contradiction by A4, A5; :: thesis: verum

end;A5: ( ((Y . 0) `) ` = the carrier of X \ ((Y . 0) `) & Ball ( the Point of X,1) c= the carrier of X ) ;

assume (Y . 0) ` = {} ; :: thesis: contradiction

hence contradiction by A4, A5; :: thesis: verum

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

reconsider t0 = min (t01,(1 / 2)) as Element of REAL by XREAL_0:def 1;

t0 <= 1 / 2 by XXREAL_0:17;

then t0 < 1 / 1 by XXREAL_0:2;

then A9: t0 < 1 / (2 |^ 0) by NEWTON:4;

Ball (z0,t0) c= Ball (z0,t01) by PCOMPS_1:1, XXREAL_0:17;

then Ball (z0,t0) c= (Y . 0) ` by A8;

then Ball (z0,t0) misses Y . 0 by SUBSET_1:23;

then A10: (Ball (z0,t0)) /\ (Y . 0) = {} by XBOOLE_0:def 7;

A11: for n being 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

ex x0 being sequence of X ex r0 being Real_Sequence st
let n be Nat; :: thesis: 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)) = {} ) )

let x be Point of X; :: thesis: 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)) = {} ) )

let r be Real; :: thesis: 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)) = {} ) )

( 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: verum

end;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)) = {} ) )

let x be Point of X; :: thesis: 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)) = {} ) )

let r be Real; :: thesis: 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)) = {} ) )

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

hence
ex x1 being Point of X ex r1 being Real st
0 < 2 |^ (n + 2)
by NEWTON:83;

then A12: 0 < 1 / (2 |^ (n + 2)) by XREAL_1:139;

0 < 2 |^ (n + 1) by NEWTON:83;

then A13: (1 / (2 |^ (n + 1))) / 2 < 1 / (2 |^ (n + 1)) by XREAL_1:139, XREAL_1:216;

2 |^ (n + 2) = 2 |^ ((n + 1) + 1)

.= (2 |^ (n + 1)) * 2 by NEWTON:6 ;

then A14: 1 / (2 |^ (n + 2)) = (1 / (2 |^ (n + 1))) / 2 by XCMPLX_1:78;

assume that

A15: 0 < r and

r < 1 / (2 |^ n) and

(Ball (x,r)) /\ (Y . n) = {} ; :: thesis: ex x1 being Point of X ex r1 being Real st S_{1}[n,x,r,x1,r1]

not Ball (x,(r / 2)) c= Y . (n + 1) by A4, A15, XREAL_1:215;

then Ball (x,(r / 2)) meets (Y . (n + 1)) ` by SUBSET_1:24;

then consider z0 being object 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:29;

then (Ball (x,(r / 2))) /\ ((Y . (n + 1)) `) in Family_open_set X by PCOMPS_1:31;

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

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

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;

then A25: Ball (x1,r1) misses Y . (n + 1) by SUBSET_1:23;

take x1 = x1; :: thesis: ex r1 being Real st S_{1}[n,x,r,x1,r1]

take r1 = r1; :: thesis: S_{1}[n,x,r,x1,r1]

A26: r1 <= 1 / (2 |^ (n + 2)) by XXREAL_0:17;

0 < min (t01,t02) by A21, A18, XXREAL_0:15;

hence S_{1}[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: verum

end;then A12: 0 < 1 / (2 |^ (n + 2)) by XREAL_1:139;

0 < 2 |^ (n + 1) by NEWTON:83;

then A13: (1 / (2 |^ (n + 1))) / 2 < 1 / (2 |^ (n + 1)) by XREAL_1:139, XREAL_1:216;

2 |^ (n + 2) = 2 |^ ((n + 1) + 1)

.= (2 |^ (n + 1)) * 2 by NEWTON:6 ;

then A14: 1 / (2 |^ (n + 2)) = (1 / (2 |^ (n + 1))) / 2 by XCMPLX_1:78;

assume that

A15: 0 < r and

r < 1 / (2 |^ n) and

(Ball (x,r)) /\ (Y . n) = {} ; :: thesis: ex x1 being Point of X ex r1 being Real st S

not Ball (x,(r / 2)) c= Y . (n + 1) by A4, A15, XREAL_1:215;

then Ball (x,(r / 2)) meets (Y . (n + 1)) ` by SUBSET_1:24;

then consider z0 being object 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:29;

then (Ball (x,(r / 2))) /\ ((Y . (n + 1)) `) in Family_open_set X by PCOMPS_1:31;

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

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

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;

then A25: Ball (x1,r1) misses Y . (n + 1) by SUBSET_1:23;

take x1 = x1; :: thesis: ex r1 being Real st S

take r1 = r1; :: thesis: S

A26: r1 <= 1 / (2 |^ (n + 2)) by XXREAL_0:17;

0 < min (t01,t02) by A21, A18, XXREAL_0:15;

hence S

( 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: verum

( x0 . 0 = z0 & r0 . 0 = t0 & ( for n being 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

then consider x0 being sequence of X, r0 being Real_Sequence such that
defpred S_{2}[ 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 Nat

for u being Element of [: the carrier of X,REAL:] ex v being Element of [: the carrier of X,REAL:] st S_{2}[n,u,v]

A29: ( f . 0 = [z0,t0] & ( for n being Nat holds S_{2}[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 2(A27);

take pr1 f ; :: thesis: ex r0 being Real_Sequence st

( (pr1 f) . 0 = z0 & r0 . 0 = t0 & ( for n being Nat st 0 < r0 . n & r0 . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),(r0 . n))) /\ (Y . n) = {} holds

( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),(r0 . (n + 1))) c= Ball (((pr1 f) . n),((r0 . n) / 2)) & (Ball (((pr1 f) . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )

take pr2 f ; :: thesis: ( (pr1 f) . 0 = z0 & (pr2 f) . 0 = t0 & ( for n being Nat st 0 < (pr2 f) . n & (pr2 f) . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),((pr2 f) . n))) /\ (Y . n) = {} holds

( 0 < (pr2 f) . (n + 1) & (pr2 f) . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1))) c= Ball (((pr1 f) . n),(((pr2 f) . n) / 2)) & (Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )

thus (pr1 f) . 0 = (f . 0) `1 by FUNCT_2:def 5

.= z0 by A29 ; :: thesis: ( (pr2 f) . 0 = t0 & ( for n being Nat st 0 < (pr2 f) . n & (pr2 f) . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),((pr2 f) . n))) /\ (Y . n) = {} holds

( 0 < (pr2 f) . (n + 1) & (pr2 f) . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1))) c= Ball (((pr1 f) . n),(((pr2 f) . n) / 2)) & (Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )

thus (pr2 f) . 0 = (f . 0) `2 by FUNCT_2:def 6

.= t0 by A29 ; :: thesis: for n being Nat st 0 < (pr2 f) . n & (pr2 f) . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),((pr2 f) . n))) /\ (Y . n) = {} holds

( 0 < (pr2 f) . (n + 1) & (pr2 f) . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1))) c= Ball (((pr1 f) . n),(((pr2 f) . n) / 2)) & (Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1)))) /\ (Y . (n + 1)) = {} )

end;A27: for n being Nat

for u being Element of [: the carrier of X,REAL:] ex v being Element of [: the carrier of X,REAL:] st S

proof

consider f being sequence of [: the carrier of X,REAL:] such that
let n be Nat; :: thesis: for u being Element of [: the carrier of X,REAL:] ex v being Element of [: the carrier of X,REAL:] st S_{2}[n,u,v]

let u be Element of [: the carrier of X,REAL:]; :: thesis: ex v being Element of [: the carrier of X,REAL:] st S_{2}[n,u,v]

consider v1 being Element of X, v2 being Real such that

A28: S_{1}[n,u `1 ,u `2 ,v1,v2]
by A11;

reconsider v2 = v2 as Element of REAL by XREAL_0:def 1;

take [v1,v2] ; :: thesis: S_{2}[n,u,[v1,v2]]

thus S_{2}[n,u,[v1,v2]]
by A28; :: thesis: verum

end;let u be Element of [: the carrier of X,REAL:]; :: thesis: ex v being Element of [: the carrier of X,REAL:] st S

consider v1 being Element of X, v2 being Real such that

A28: S

reconsider v2 = v2 as Element of REAL by XREAL_0:def 1;

take [v1,v2] ; :: thesis: S

thus S

A29: ( f . 0 = [z0,t0] & ( for n being Nat holds S

take pr1 f ; :: thesis: ex r0 being Real_Sequence st

( (pr1 f) . 0 = z0 & r0 . 0 = t0 & ( for n being Nat st 0 < r0 . n & r0 . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),(r0 . n))) /\ (Y . n) = {} holds

( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),(r0 . (n + 1))) c= Ball (((pr1 f) . n),((r0 . n) / 2)) & (Ball (((pr1 f) . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )

take pr2 f ; :: thesis: ( (pr1 f) . 0 = z0 & (pr2 f) . 0 = t0 & ( for n being Nat st 0 < (pr2 f) . n & (pr2 f) . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),((pr2 f) . n))) /\ (Y . n) = {} holds

( 0 < (pr2 f) . (n + 1) & (pr2 f) . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1))) c= Ball (((pr1 f) . n),(((pr2 f) . n) / 2)) & (Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )

thus (pr1 f) . 0 = (f . 0) `1 by FUNCT_2:def 5

.= z0 by A29 ; :: thesis: ( (pr2 f) . 0 = t0 & ( for n being Nat st 0 < (pr2 f) . n & (pr2 f) . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),((pr2 f) . n))) /\ (Y . n) = {} holds

( 0 < (pr2 f) . (n + 1) & (pr2 f) . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1))) c= Ball (((pr1 f) . n),(((pr2 f) . n) / 2)) & (Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1)))) /\ (Y . (n + 1)) = {} ) ) )

thus (pr2 f) . 0 = (f . 0) `2 by FUNCT_2:def 6

.= t0 by A29 ; :: thesis: for n being Nat st 0 < (pr2 f) . n & (pr2 f) . n < 1 / (2 |^ n) & (Ball (((pr1 f) . n),((pr2 f) . n))) /\ (Y . n) = {} holds

( 0 < (pr2 f) . (n + 1) & (pr2 f) . (n + 1) < 1 / (2 |^ (n + 1)) & Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1))) c= Ball (((pr1 f) . n),(((pr2 f) . n) / 2)) & (Ball (((pr1 f) . (n + 1)),((pr2 f) . (n + 1)))) /\ (Y . (n + 1)) = {} )

hereby :: thesis: verum

let i be Nat; :: thesis: S_{1}[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)]

A30: i in NAT by ORDINAL1:def 12;

A31: ( (f . (i + 1)) `1 = (pr1 f) . (i + 1) & (f . (i + 1)) `2 = (pr2 f) . (i + 1) ) by FUNCT_2:def 5, FUNCT_2:def 6;

( (f . i) `1 = (pr1 f) . i & (f . i) `2 = (pr2 f) . i ) by FUNCT_2:def 5, FUNCT_2:def 6, A30;

hence S_{1}[i,(pr1 f) . i,(pr2 f) . i,(pr1 f) . (i + 1),(pr2 f) . (i + 1)]
by A29, A31; :: thesis: verum

end;A30: i in NAT by ORDINAL1:def 12;

A31: ( (f . (i + 1)) `1 = (pr1 f) . (i + 1) & (f . (i + 1)) `2 = (pr2 f) . (i + 1) ) by FUNCT_2:def 5, FUNCT_2:def 6;

( (f . i) `1 = (pr1 f) . i & (f . i) `2 = (pr2 f) . i ) by FUNCT_2:def 5, FUNCT_2:def 6, A30;

hence S

A32: ( x0 . 0 = z0 & r0 . 0 = t0 ) and

A33: for n being 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 A34: 0 < t0 by A7, XXREAL_0:15;

A35: for n being 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

A40:
for m, k being Nat holds dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))
defpred S_{2}[ 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) = {} );

_{2}[ 0 ]
by A34, A9, A10, A32, A33;

thus for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A39, A36); :: thesis: verum

end;A36: now :: thesis: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]

A39:
SS

let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A37: S_{2}[n]
; :: thesis: S_{2}[n + 1]

then A38: (Ball ((x0 . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1)) = {} by A33;

( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) ) by A33, A37;

hence S_{2}[n + 1]
by A33, A38; :: thesis: verum

end;assume A37: S

then A38: (Ball ((x0 . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1)) = {} by A33;

( 0 < r0 . (n + 1) & r0 . (n + 1) < 1 / (2 |^ (n + 1)) ) by A33, A37;

hence S

thus for n being Nat holds S

proof

let m be Nat; :: thesis: for k being Nat holds dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))

defpred S_{2}[ Nat] means dist ((x0 . (m + $1)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ $1)));

then A47: S_{2}[ 0 ]
by METRIC_1:1;

for k being Nat holds S_{2}[k]
from NAT_1:sch 2(A47, A41);

hence for k being Nat holds dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) ; :: thesis: verum

end;defpred S

A41: now :: thesis: for k being Nat st S_{2}[k] holds

S_{2}[k + 1]

2 |^ 0 = 1
by NEWTON:4;S

let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume S_{2}[k]
; :: thesis: S_{2}[k + 1]

then A42: (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:6;

( 0 < r0 . ((m + k) + 1) & dist ((x0 . ((m + k) + 1)),(x0 . ((m + k) + 1))) = 0 ) by A35, METRIC_1:1;

then A43: x0 . ((m + k) + 1) in Ball ((x0 . ((m + k) + 1)),(r0 . ((m + k) + 1))) by METRIC_1:11;

r0 . (m + k) < 1 / (2 |^ (m + k)) by A35;

then (r0 . (m + k)) / 2 < (1 / (2 |^ (m + k))) / 2 by XREAL_1:74;

then (r0 . (m + k)) / 2 < 1 / ((2 |^ (m + k)) * 2) by XCMPLX_1:78;

then A44: (r0 . (m + k)) / 2 < 1 / (2 |^ ((m + k) + 1)) by NEWTON:6;

Ball ((x0 . ((m + k) + 1)),(r0 . ((m + k) + 1))) c= Ball ((x0 . (m + k)),((r0 . (m + k)) / 2)) by A35;

then dist ((x0 . ((m + k) + 1)),(x0 . (m + k))) < (r0 . (m + k)) / 2 by A43, METRIC_1:11;

then dist ((x0 . ((m + k) + 1)),(x0 . (m + k))) <= 1 / (2 |^ ((m + k) + 1)) by A44, XXREAL_0:2;

then A45: (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:6;

2 |^ (m + (k + 1)) = (2 |^ m) * (2 |^ (k + 1)) by NEWTON:8;

then 1 / (2 |^ ((m + k) + 1)) = (1 / (2 |^ m)) / ((2 |^ (k + 1)) / 1) by XCMPLX_1:78

.= (1 / (2 |^ m)) * (1 / (2 |^ (k + 1))) by XCMPLX_1:79 ;

then A46: (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:6

.= (1 / (2 |^ m)) * (1 + (((1 / (2 |^ k)) / 2) - (1 / (2 |^ k)))) by XCMPLX_1:78

.= (1 / (2 |^ m)) * (1 - ((1 / (2 |^ k)) / 2))

.= (1 / (2 |^ m)) * (1 - (1 / ((2 |^ k) * 2))) by XCMPLX_1:78 ;

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 A42, XXREAL_0:2;

then dist ((x0 . (m + (k + 1))),(x0 . m)) <= (1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by A45, XXREAL_0:2;

hence S_{2}[k + 1]
by A46, NEWTON:6; :: thesis: verum

end;assume S

then A42: (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:6;

( 0 < r0 . ((m + k) + 1) & dist ((x0 . ((m + k) + 1)),(x0 . ((m + k) + 1))) = 0 ) by A35, METRIC_1:1;

then A43: x0 . ((m + k) + 1) in Ball ((x0 . ((m + k) + 1)),(r0 . ((m + k) + 1))) by METRIC_1:11;

r0 . (m + k) < 1 / (2 |^ (m + k)) by A35;

then (r0 . (m + k)) / 2 < (1 / (2 |^ (m + k))) / 2 by XREAL_1:74;

then (r0 . (m + k)) / 2 < 1 / ((2 |^ (m + k)) * 2) by XCMPLX_1:78;

then A44: (r0 . (m + k)) / 2 < 1 / (2 |^ ((m + k) + 1)) by NEWTON:6;

Ball ((x0 . ((m + k) + 1)),(r0 . ((m + k) + 1))) c= Ball ((x0 . (m + k)),((r0 . (m + k)) / 2)) by A35;

then dist ((x0 . ((m + k) + 1)),(x0 . (m + k))) < (r0 . (m + k)) / 2 by A43, METRIC_1:11;

then dist ((x0 . ((m + k) + 1)),(x0 . (m + k))) <= 1 / (2 |^ ((m + k) + 1)) by A44, XXREAL_0:2;

then A45: (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:6;

2 |^ (m + (k + 1)) = (2 |^ m) * (2 |^ (k + 1)) by NEWTON:8;

then 1 / (2 |^ ((m + k) + 1)) = (1 / (2 |^ m)) / ((2 |^ (k + 1)) / 1) by XCMPLX_1:78

.= (1 / (2 |^ m)) * (1 / (2 |^ (k + 1))) by XCMPLX_1:79 ;

then A46: (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:6

.= (1 / (2 |^ m)) * (1 + (((1 / (2 |^ k)) / 2) - (1 / (2 |^ k)))) by XCMPLX_1:78

.= (1 / (2 |^ m)) * (1 - ((1 / (2 |^ k)) / 2))

.= (1 / (2 |^ m)) * (1 - (1 / ((2 |^ k) * 2))) by XCMPLX_1:78 ;

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 A42, XXREAL_0:2;

then dist ((x0 . (m + (k + 1))),(x0 . m)) <= (1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by A45, XXREAL_0:2;

hence S

then A47: S

for k being Nat holds S

hence for k being Nat holds dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) ; :: thesis: verum

A48: now :: thesis: for m, k being Nat holds dist ((x0 . (m + k)),(x0 . m)) < 1 / (2 |^ m)

let m be Nat; :: thesis: for k being Nat holds dist ((x0 . (m + k)),(x0 . m)) < 1 / (2 |^ m)

end;hereby :: thesis: verum

let k be Nat; :: thesis: dist ((x0 . (m + k)),(x0 . m)) < 1 / (2 |^ m)

A49: dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) by A40;

0 < 2 |^ k by NEWTON:83;

then 0 < 1 / (2 |^ k) by XREAL_1:139;

then A50: 1 - (1 / (2 |^ k)) < 1 - 0 by XREAL_1:10;

0 < 2 |^ m by NEWTON:83;

then 0 < 1 / (2 |^ m) by XREAL_1:139;

then (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) < (1 / (2 |^ m)) * 1 by A50, XREAL_1:68;

hence dist ((x0 . (m + k)),(x0 . m)) < 1 / (2 |^ m) by A49, XXREAL_0:2; :: thesis: verum

end;A49: dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) by A40;

0 < 2 |^ k by NEWTON:83;

then 0 < 1 / (2 |^ k) by XREAL_1:139;

then A50: 1 - (1 / (2 |^ k)) < 1 - 0 by XREAL_1:10;

0 < 2 |^ m by NEWTON:83;

then 0 < 1 / (2 |^ m) by XREAL_1:139;

then (1 / (2 |^ m)) * (1 - (1 / (2 |^ k))) < (1 / (2 |^ m)) * 1 by A50, XREAL_1:68;

hence dist ((x0 . (m + k)),(x0 . m)) < 1 / (2 |^ m) by A49, XXREAL_0:2; :: thesis: verum

now :: thesis: for r being Real st 0 < r holds

ex p being Nat st

for n, m being Nat st n >= p & m >= p holds

dist ((x0 . n),(x0 . m)) < r

then
x0 is Cauchy
by TBSP_1:def 4;ex p being Nat st

for n, m being Nat st n >= p & m >= p holds

dist ((x0 . n),(x0 . m)) < r

let r be Real; :: thesis: ( 0 < r implies ex p being Nat st

for n, m being Nat st n >= p & m >= p holds

dist ((x0 . n),(x0 . m)) < r )

assume 0 < r ; :: thesis: ex p being Nat st

for n, m being Nat st n >= p & m >= p holds

dist ((x0 . n),(x0 . m)) < r

then consider p1 being Nat such that

A51: 1 / (2 |^ p1) <= r by PREPOWER:92;

reconsider p = p1 + 1 as Nat ;

take p = p; :: thesis: for n, m being Nat st n >= p & m >= p holds

dist ((x0 . n),(x0 . m)) < r

end;for n, m being Nat st n >= p & m >= p holds

dist ((x0 . n),(x0 . m)) < r )

assume 0 < r ; :: thesis: ex p being Nat st

for n, m being Nat st n >= p & m >= p holds

dist ((x0 . n),(x0 . m)) < r

then consider p1 being Nat such that

A51: 1 / (2 |^ p1) <= r by PREPOWER:92;

reconsider p = p1 + 1 as Nat ;

take p = p; :: thesis: for n, m being Nat st n >= p & m >= p holds

dist ((x0 . n),(x0 . m)) < r

hereby :: thesis: verum

let n, m be Nat; :: thesis: ( n >= p & m >= p implies dist ((x0 . n),(x0 . m)) < r )

assume that

A52: n >= p and

A53: m >= p ; :: thesis: dist ((x0 . n),(x0 . m)) < r

consider k1 being Nat such that

A54: n = p + k1 by A52, NAT_1:10;

reconsider k1 = k1 as Nat ;

n = p + k1 by A54;

then A55: dist ((x0 . n),(x0 . p)) < 1 / (2 |^ p) by A48;

consider k2 being Nat such that

A56: m = p + k2 by A53, NAT_1:10;

reconsider k2 = k2 as Nat ;

A57: 1 / (2 |^ p) = 1 / ((2 |^ p1) * 2) by NEWTON:6

.= (1 / (2 |^ p1)) / 2 by XCMPLX_1:78 ;

m = p + k2 by A56;

then A58: (dist ((x0 . n),(x0 . p))) + (dist ((x0 . p),(x0 . m))) < (1 / (2 |^ p)) + (1 / (2 |^ p)) by A48, A55, XREAL_1:8;

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 A58, A57, XXREAL_0:2;

hence dist ((x0 . n),(x0 . m)) < r by A51, XXREAL_0:2; :: thesis: verum

end;assume that

A52: n >= p and

A53: m >= p ; :: thesis: dist ((x0 . n),(x0 . m)) < r

consider k1 being Nat such that

A54: n = p + k1 by A52, NAT_1:10;

reconsider k1 = k1 as Nat ;

n = p + k1 by A54;

then A55: dist ((x0 . n),(x0 . p)) < 1 / (2 |^ p) by A48;

consider k2 being Nat such that

A56: m = p + k2 by A53, NAT_1:10;

reconsider k2 = k2 as Nat ;

A57: 1 / (2 |^ p) = 1 / ((2 |^ p1) * 2) by NEWTON:6

.= (1 / (2 |^ p1)) / 2 by XCMPLX_1:78 ;

m = p + k2 by A56;

then A58: (dist ((x0 . n),(x0 . p))) + (dist ((x0 . p),(x0 . m))) < (1 / (2 |^ p)) + (1 / (2 |^ p)) by A48, A55, XREAL_1:8;

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 A58, A57, XXREAL_0:2;

hence dist ((x0 . n),(x0 . m)) < r by A51, XXREAL_0:2; :: thesis: verum

then A59: x0 is convergent by A1, TBSP_1:def 5;

A60: for m, k being Nat holds Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) c= Ball ((x0 . m),((r0 . m) / 2))

proof

let m be Nat; :: thesis: for k being Nat holds Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) c= Ball ((x0 . m),((r0 . m) / 2))

defpred S_{2}[ Nat] means Ball ((x0 . ((m + 1) + $1)),(r0 . ((m + 1) + $1))) c= Ball ((x0 . m),((r0 . m) / 2));

_{2}[ 0 ]
by A35;

thus for k being Nat holds S_{2}[k]
from NAT_1:sch 2(A64, A61); :: thesis: verum

end;defpred S

A61: now :: thesis: for k being Nat st S_{2}[k] holds

S_{2}[k + 1]

A64:
SS

let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume A62: S_{2}[k]
; :: thesis: S_{2}[k + 1]

0 < r0 . ((m + 1) + k) by A35;

then (r0 . ((m + 1) + k)) / 2 < r0 . ((m + 1) + k) by XREAL_1:216;

then A63: 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 A35;

then Ball ((x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1)))) c= Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) by A63;

hence S_{2}[k + 1]
by A62, XBOOLE_1:1; :: thesis: verum

end;assume A62: S

0 < r0 . ((m + 1) + k) by A35;

then (r0 . ((m + 1) + k)) / 2 < r0 . ((m + 1) + k) by XREAL_1:216;

then A63: 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 A35;

then Ball ((x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1)))) c= Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k))) by A63;

hence S

thus for k being Nat holds S

A65: now :: thesis: for m being Nat holds lim x0 in Ball ((x0 . m),(r0 . m))

let m be Nat; :: thesis: lim x0 in Ball ((x0 . m),(r0 . m))

set m1 = m + 1;

0 < r0 . m by A35;

then 0 < (r0 . m) / 2 by XREAL_1:215;

then consider n1 being Nat such that

A66: for l being Nat st n1 <= l holds

dist ((x0 . l),(lim x0)) < (r0 . m) / 2 by A59, TBSP_1:def 3;

reconsider n = max (n1,(m + 1)) as Nat by TARSKI:1;

A67: dist ((x0 . n),(lim x0)) < (r0 . m) / 2 by A66, XXREAL_0:25;

consider k being Nat such that

A68: n = (m + 1) + k by NAT_1:10, XXREAL_0:25;

( dist ((x0 . n),(x0 . n)) = 0 & 0 < r0 . n ) by A35, METRIC_1:1;

then A69: x0 . n in Ball ((x0 . n),(r0 . n)) by METRIC_1:11;

reconsider k = k as Nat ;

n = (m + 1) + k by A68;

then Ball ((x0 . n),(r0 . n)) c= Ball ((x0 . m),((r0 . m) / 2)) by A60;

then dist ((x0 . n),(x0 . m)) < (r0 . m) / 2 by A69, METRIC_1:11;

then A70: (dist ((lim x0),(x0 . n))) + (dist ((x0 . n),(x0 . m))) < ((r0 . m) / 2) + ((r0 . m) / 2) by A67, XREAL_1:8;

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 A70, XXREAL_0:2;

hence lim x0 in Ball ((x0 . m),(r0 . m)) by METRIC_1:11; :: thesis: verum

end;set m1 = m + 1;

0 < r0 . m by A35;

then 0 < (r0 . m) / 2 by XREAL_1:215;

then consider n1 being Nat such that

A66: for l being Nat st n1 <= l holds

dist ((x0 . l),(lim x0)) < (r0 . m) / 2 by A59, TBSP_1:def 3;

reconsider n = max (n1,(m + 1)) as Nat by TARSKI:1;

A67: dist ((x0 . n),(lim x0)) < (r0 . m) / 2 by A66, XXREAL_0:25;

consider k being Nat such that

A68: n = (m + 1) + k by NAT_1:10, XXREAL_0:25;

( dist ((x0 . n),(x0 . n)) = 0 & 0 < r0 . n ) by A35, METRIC_1:1;

then A69: x0 . n in Ball ((x0 . n),(r0 . n)) by METRIC_1:11;

reconsider k = k as Nat ;

n = (m + 1) + k by A68;

then Ball ((x0 . n),(r0 . n)) c= Ball ((x0 . m),((r0 . m) / 2)) by A60;

then dist ((x0 . n),(x0 . m)) < (r0 . m) / 2 by A69, METRIC_1:11;

then A70: (dist ((lim x0),(x0 . n))) + (dist ((x0 . n),(x0 . m))) < ((r0 . m) / 2) + ((r0 . m) / 2) by A67, XREAL_1:8;

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 A70, XXREAL_0:2;

hence lim x0 in Ball ((x0 . m),(r0 . m)) by METRIC_1:11; :: thesis: verum

A71: now :: thesis: for n being Nat holds not lim x0 in Y . nend;

not lim x0 in union (rng Y)
proof

hence
contradiction
by A2; :: thesis: verum
assume
lim x0 in union (rng Y)
; :: thesis: contradiction

then consider A being set such that

A73: lim x0 in A and

A74: A in rng Y by TARSKI:def 4;

ex k being object st

( k in dom Y & A = Y . k ) by A74, FUNCT_1:def 3;

hence contradiction by A71, A73; :: thesis: verum

end;then consider A being set such that

A73: lim x0 in A and

A74: A in rng Y by TARSKI:def 4;

ex k being object st

( k in dom Y & A = Y . k ) by A74, FUNCT_1:def 3;

hence contradiction by A71, A73; :: thesis: verum