let X be non empty MetrSpace; 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; ( 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
; ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
defpred S1[ 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 )
; contradiction
then consider z0 being object 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 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
let n be
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)) = {} ) )let x be
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 r be
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)) = {} ) )
now ( 0 < r & r < 1 / (2 |^ n) & (Ball (x,r)) /\ (Y . n) = {} implies ex x1 being Point of X ex r1 being Real st S1[n,x,r,x1,r1] )
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) = {}
;
ex x1 being Point of X ex r1 being Real st S1[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;
ex r1 being Real st S1[n,x,r,x1,r1]take r1 =
r1;
S1[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
S1[
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;
verum 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)) = {} ) )
;
verum
end;
ex x0 being sequence of X ex r0 being Real_Sequence st
( 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
defpred S2[
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
S2[
n,
u,
v]
proof
let n be
Nat;
for u being Element of [: the carrier of X,REAL:] ex v being Element of [: the carrier of X,REAL:] st S2[n,u,v]let u be
Element of
[: the carrier of X,REAL:];
ex v being Element of [: the carrier of X,REAL:] st S2[n,u,v]
consider v1 being
Element of
X,
v2 being
Real such that A28:
S1[
n,
u `1 ,
u `2 ,
v1,
v2]
by A11;
reconsider v2 =
v2 as
Element of
REAL by XREAL_0:def 1;
take
[v1,v2]
;
S2[n,u,[v1,v2]]
thus
S2[
n,
u,
[v1,v2]]
by A28;
verum
end;
consider f being
sequence of
[: the carrier of X,REAL:] such that A29:
(
f . 0 = [z0,t0] & ( for
n being
Nat holds
S2[
n,
f . n,
f . (n + 1)] ) )
from RECDEF_1:sch 2(A27);
take
pr1 f
;
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
;
( (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
;
( (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
;
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 verum
let i be
Nat;
S1[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
S1[
i,
(pr1 f) . i,
(pr2 f) . i,
(pr1 f) . (i + 1),
(pr2 f) . (i + 1)]
by A29, A31;
verum
end;
end;
then consider x0 being sequence of X, r0 being Real_Sequence such that
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
defpred S2[
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) = {} );
A36:
now for n being Nat st S2[n] holds
S2[n + 1]let n be
Nat;
( S2[n] implies S2[n + 1] )assume A37:
S2[
n]
;
S2[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
S2[
n + 1]
by A33, A38;
verum end;
A39:
S2[
0 ]
by A34, A9, A10, A32, A33;
thus
for
n being
Nat holds
S2[
n]
from NAT_1:sch 2(A39, A36); verum
end;
A40:
for m, k being Nat holds dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))
proof
let m be
Nat;
for k being Nat holds dist ((x0 . (m + k)),(x0 . m)) <= (1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))
defpred S2[
Nat]
means dist (
(x0 . (m + $1)),
(x0 . m))
<= (1 / (2 |^ m)) * (1 - (1 / (2 |^ $1)));
A41:
now for k being Nat st S2[k] holds
S2[k + 1]let k be
Nat;
( S2[k] implies S2[k + 1] )assume
S2[
k]
;
S2[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
S2[
k + 1]
by A46, NEWTON:6;
verum end;
2
|^ 0 = 1
by NEWTON:4;
then A47:
S2[
0 ]
by METRIC_1:1;
for
k being
Nat holds
S2[
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)))
;
verum
end;
now 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)) < rlet r be
Real;
( 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
;
ex p being Nat st
for n, m being Nat st n >= p & m >= p holds
dist ((x0 . n),(x0 . m)) < rthen consider p1 being
Nat such that A51:
1
/ (2 |^ p1) <= r
by PREPOWER:92;
reconsider p =
p1 + 1 as
Nat ;
take p =
p;
for n, m being Nat st n >= p & m >= p holds
dist ((x0 . n),(x0 . m)) < rhereby verum
let n,
m be
Nat;
( n >= p & m >= p implies dist ((x0 . n),(x0 . m)) < r )assume that A52:
n >= p
and A53:
m >= p
;
dist ((x0 . n),(x0 . m)) < rconsider 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;
verum
end; end;
then
x0 is Cauchy
by TBSP_1:def 4;
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))
A65:
now for m being Nat holds lim x0 in Ball ((x0 . m),(r0 . m))let m be
Nat;
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;
verum end;
not lim x0 in union (rng Y)
hence
contradiction
by A2; verum