:: METRIC_6 semantic presentation

begin


theorem Th1: :: METRIC_6:1
for X being MetrSpace
for x, z, y being Element of X holds abs ((dist (x,z)) - (dist (y,z))) <= dist (x,y)
proof
let X be MetrSpace; ::_thesis: for x, z, y being Element of X holds abs ((dist (x,z)) - (dist (y,z))) <= dist (x,y)
let x, z, y be Element of X; ::_thesis: abs ((dist (x,z)) - (dist (y,z))) <= dist (x,y)
 dist (y,z) <= (dist (y,x)) + (dist (x,z)) by METRIC_1:4;
then  (dist (y,z)) - (dist (x,z)) <= dist (x,y) by XREAL_1:20;
then A1: - (dist (x,y)) <= - ((dist (y,z)) - (dist (x,z))) by XREAL_1:24;
 dist (x,z) <= (dist (x,y)) + (dist (y,z)) by METRIC_1:4;
then  (dist (x,z)) - (dist (y,z)) <= dist (x,y) by XREAL_1:20;
hence  abs ((dist (x,z)) - (dist (y,z))) <= dist (x,y) by A1, ABSVALUE:5; ::_thesis: verum
end;

theorem Th2: :: METRIC_6:2
for A being non empty set
for G being Function of [:A,A:],REAL st G is_metric_of A holds
for a, b being Element of A holds 0 <= G . (a,b)
proof
let A be non empty set ; ::_thesis: for G being Function of [:A,A:],REAL st G is_metric_of A holds
for a, b being Element of A holds 0 <= G . (a,b)
let G be Function of [:A,A:],REAL; ::_thesis: ( G is_metric_of A implies for a, b being Element of A holds 0 <= G . (a,b) )
assume A1: G is_metric_of A ; ::_thesis: for a, b being Element of A holds 0 <= G . (a,b)
let a, b be Element of A; ::_thesis: 0 <= G . (a,b)
A2: (1 / 2) * (G . (a,a)) = (1 / 2) * 0 by A1, PCOMPS_1:def_6;
G . (a,b) = (1 / 2) * ((1 * (G . (a,b))) + (G . (a,b)))
.= (1 / 2) * ((G . (a,b)) + (G . (b,a))) by A1, PCOMPS_1:def_6 ;
hence  0 <= G . (a,b) by A1, A2, PCOMPS_1:def_6; ::_thesis: verum
end;

theorem Th3: :: METRIC_6:3
for A being non empty set
for G being Function of [:A,A:],REAL holds
( G is_metric_of A iff ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) )
proof
let A be non empty set ; ::_thesis: for G being Function of [:A,A:],REAL holds
( G is_metric_of A iff ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) )
let G be Function of [:A,A:],REAL; ::_thesis: ( G is_metric_of A iff ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) )
A1: ( G is_metric_of A implies ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) )
proof
assume A2: G is_metric_of A ; ::_thesis: ( G is Reflexive & G is discerning & G is symmetric & G is triangle )
then  for a being Element of A holds G . (a,a) = 0 by PCOMPS_1:def_6;
hence  G is Reflexive by METRIC_1:def_2; ::_thesis: ( G is discerning & G is symmetric & G is triangle )
 for a, b being Element of A holds
( G . (a,b) = 0 iff a = b ) by A2, PCOMPS_1:def_6;
hence  G is discerning by METRIC_1:def_3; ::_thesis: ( G is symmetric & G is triangle )
 for a, b being Element of A holds G . (a,b) = G . (b,a) by A2, PCOMPS_1:def_6;
hence  G is symmetric by METRIC_1:def_4; ::_thesis: G is triangle
 for a, b, c being Element of A holds G . (a,c) <= (G . (a,b)) + (G . (b,c)) by A2, PCOMPS_1:def_6;
hence  G is triangle by METRIC_1:def_5; ::_thesis: verum
end;
 ( G is Reflexive & G is discerning & G is symmetric & G is triangle implies G is_metric_of A )
proof
assume  ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) ; ::_thesis: G is_metric_of A
then  for a, b, c being Element of A holds
( ( G . (a,b) = 0 implies a = b ) & ( a = b implies G . (a,b) = 0 ) & G . (a,b) = G . (b,a) & G . (a,c) <= (G . (a,b)) + (G . (b,c)) ) by METRIC_1:def_2, METRIC_1:def_3, METRIC_1:def_4, METRIC_1:def_5;
hence  G is_metric_of A by PCOMPS_1:def_6; ::_thesis: verum
end;
hence  ( G is_metric_of A iff ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) ) by A1; ::_thesis: verum
end;

theorem :: METRIC_6:4
for X being non empty strict MetrSpace holds
( the distance of X is Reflexive & the distance of X is discerning & the distance of X is symmetric & the distance of X is triangle )
proof
let X be non empty strict MetrSpace; ::_thesis: ( the distance of X is Reflexive & the distance of X is discerning & the distance of X is symmetric & the distance of X is triangle )
A1: the distance of X is_metric_of the carrier of X by PCOMPS_1:35;
hence  the distance of X is Reflexive by Th3; ::_thesis: ( the distance of X is discerning & the distance of X is symmetric & the distance of X is triangle )
thus  the distance of X is discerning by A1, Th3; ::_thesis: ( the distance of X is symmetric & the distance of X is triangle )
thus  the distance of X is symmetric by A1, Th3; ::_thesis: the distance of X is triangle
thus  the distance of X is triangle by A1, Th3; ::_thesis: verum
end;

theorem :: METRIC_6:5
for A being non empty set
for G being Function of [:A,A:],REAL holds
( G is_metric_of A iff ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) )
proof
let A be non empty set ; ::_thesis: for G being Function of [:A,A:],REAL holds
( G is_metric_of A iff ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) )
let G be Function of [:A,A:],REAL; ::_thesis: ( G is_metric_of A iff ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) )
A1: ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) implies G is_metric_of A )
proof
assume that
A2: ( G is Reflexive & G is discerning ) and
A3: for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ; ::_thesis: G is_metric_of A
A4: for b, c being Element of A holds G . (b,c) = G . (c,b)
proof
let b, c be Element of A; ::_thesis: G . (b,c) = G . (c,b)
 G . (c,b) <= (G . (b,c)) + (G . (b,b)) by A3;
then A5: G . (c,b) <= (G . (b,c)) + 0 by A2, METRIC_1:def_2;
 G . (b,c) <= (G . (c,b)) + (G . (c,c)) by A3;
then  G . (b,c) <= (G . (c,b)) + 0 by A2, METRIC_1:def_2;
hence  G . (b,c) = G . (c,b) by A5, XXREAL_0:1; ::_thesis: verum
end;
 for a, b, c being Element of A holds G . (a,c) <= (G . (a,b)) + (G . (b,c))
proof
let a, b, c be Element of A; ::_thesis: G . (a,c) <= (G . (a,b)) + (G . (b,c))
 G . (a,c) <= (G . (b,a)) + (G . (b,c)) by A3;
hence  G . (a,c) <= (G . (a,b)) + (G . (b,c)) by A4; ::_thesis: verum
end;
then  ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) by A2, A4, METRIC_1:def_4, METRIC_1:def_5;
hence  G is_metric_of A by Th3; ::_thesis: verum
end;
 ( G is_metric_of A implies ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) )
proof
assume A6: G is_metric_of A ; ::_thesis: ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) )
then A7: ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) by Th3;
now__::_thesis:_for_a,_b,_c_being_Element_of_A_holds_G_._(b,c)_<=_(G_._(a,b))_+_(G_._(a,c))
let a, b, c be Element of A; ::_thesis: G . (b,c) <= (G . (a,b)) + (G . (a,c))
 G . (b,c) <= (G . (b,a)) + (G . (a,c)) by A7, METRIC_1:def_5;
hence  G . (b,c) <= (G . (a,b)) + (G . (a,c)) by A7, METRIC_1:def_4; ::_thesis: verum
end;
hence  ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) by A6, Th3; ::_thesis: verum
end;
hence  ( G is_metric_of A iff ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) ) by A1; ::_thesis: verum
end;

definition
let A be non empty set ;
let G be Function of [:A,A:],REAL;
func bounded_metric (A,G) ->  Function of [:A,A:],REAL means :Def1: :: METRIC_6:def 1
 for a, b being Element of A holds it . (a,b) = (G . (a,b)) / (1 + (G . (a,b)));
existence
 ex b1 being Function of [:A,A:],REAL st
for a, b being Element of A holds b1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b)))
proof
deffunc H1( Element of A, Element of A) ->  Element of REAL = (G . ($1,$2)) / (1 + (G . ($1,$2)));
consider F being Function of [:A,A:],REAL such that
A1: for a, b being Element of A holds F . (a,b) = H1(a,b) from BINOP_1:sch_4();
take  F ; ::_thesis: for a, b being Element of A holds F . (a,b) = (G . (a,b)) / (1 + (G . (a,b)))
let a, b be Element of A; ::_thesis: F . (a,b) = (G . (a,b)) / (1 + (G . (a,b)))
thus  F . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:A,A:],REAL st ( for a, b being Element of A holds b1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) & ( for a, b being Element of A holds b2 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) holds
b1 = b2
proof
let f1, f2 be Function of [:A,A:],REAL; ::_thesis: ( ( for a, b being Element of A holds f1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) & ( for a, b being Element of A holds f2 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) implies f1 = f2 )
assume that
A2: for a, b being Element of A holds f1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) and
A3: for a, b being Element of A holds f2 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ; ::_thesis: f1 = f2
 for a, b being Element of A holds f1 . (a,b) = f2 . (a,b)
proof
let a, b be Element of A; ::_thesis: f1 . (a,b) = f2 . (a,b)
 f1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) by A2;
hence  f1 . (a,b) = f2 . (a,b) by A3; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines bounded_metric METRIC_6:def_1_:_
 for A being non empty set
for G, b3 being Function of [:A,A:],REAL holds
( b3 = bounded_metric (A,G) iff for a, b being Element of A holds b3 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) );

theorem :: METRIC_6:6
for A being non empty set
for G being Function of [:A,A:],REAL st G is_metric_of A holds
bounded_metric (A,G) is_metric_of A
proof
let A be non empty set ; ::_thesis: for G being Function of [:A,A:],REAL st G is_metric_of A holds
bounded_metric (A,G) is_metric_of A
let G be Function of [:A,A:],REAL; ::_thesis: ( G is_metric_of A implies bounded_metric (A,G) is_metric_of A )
assume A1: G is_metric_of A ; ::_thesis: bounded_metric (A,G) is_metric_of A
A2: for a, b, c being Element of A holds (bounded_metric (A,G)) . (a,c) <= ((bounded_metric (A,G)) . (a,b)) + ((bounded_metric (A,G)) . (b,c))
proof
let a, b, c be Element of A; ::_thesis: (bounded_metric (A,G)) . (a,c) <= ((bounded_metric (A,G)) . (a,b)) + ((bounded_metric (A,G)) . (b,c))
set a1 = G . (a,b);
set a3 = G . (a,c);
set a5 = G . (b,c);
A3: ( (bounded_metric (A,G)) . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) & (bounded_metric (A,G)) . (a,c) = (G . (a,c)) / (1 + (G . (a,c))) ) by Def1;
A4: (bounded_metric (A,G)) . (b,c) = (G . (b,c)) / (1 + (G . (b,c))) by Def1;
A5: G . (a,c) >= 0 by A1, Th2;
A6: ( 0 <= G . (a,b) & 0 <= G . (b,c) ) by A1, Th2;
then A7: 0 <> (1 + (G . (a,b))) * (1 + (G . (b,c))) by XCMPLX_1:6;
A8: ((G . (a,b)) / (1 + (G . (a,b)))) + ((G . (b,c)) / (1 + (G . (b,c)))) = (((G . (a,b)) * (1 + (G . (b,c)))) + ((G . (b,c)) * (1 + (G . (a,b))))) / ((1 + (G . (a,b))) * (1 + (G . (b,c)))) by A6, XCMPLX_1:116
.= ((((G . (a,b)) * 1) + ((G . (a,b)) * (G . (b,c)))) + (((G . (b,c)) * 1) + ((G . (b,c)) * (G . (a,b))))) / ((1 + (G . (a,b))) * (1 + (G . (b,c)))) ;
 0 <= G . (a,c) by A1, Th2;
then A9: (((G . (a,b)) / (1 + (G . (a,b)))) + ((G . (b,c)) / (1 + (G . (b,c))))) - ((G . (a,c)) / (1 + (G . (a,c)))) = (((((G . (a,b)) + ((G . (a,b)) * (G . (b,c)))) + ((G . (b,c)) + ((G . (b,c)) * (G . (a,b))))) * (1 + (G . (a,c)))) - ((G . (a,c)) * ((1 + (G . (a,b))) * (1 + (G . (b,c)))))) / (((1 + (G . (a,b))) * (1 + (G . (b,c)))) * (1 + (G . (a,c)))) by A7, A8, XCMPLX_1:130;
A10: ( G . (a,b) >= 0 & G . (b,c) >= 0 ) by A1, Th2;
 G . (a,c) <= (G . (a,b)) + (G . (b,c)) by A1, PCOMPS_1:def_6;
then  ((G . (a,b)) + (G . (b,c))) - (G . (a,c)) >= 0 by XREAL_1:48;
then  (((G . (b,c)) + (G . (a,b))) - (G . (a,c))) + (((G . (a,b)) * (G . (b,c))) + (((G . (b,c)) * (G . (a,b))) + (((G . (b,c)) * (G . (a,b))) * (G . (a,c))))) >= 0 by A10, A5;
hence  (bounded_metric (A,G)) . (a,c) <= ((bounded_metric (A,G)) . (a,b)) + ((bounded_metric (A,G)) . (b,c)) by A3, A4, A9, A10, A5, XREAL_1:49; ::_thesis: verum
end;
A11: for a, b being Element of A holds
( (bounded_metric (A,G)) . (a,b) = 0 iff a = b )
proof
let a, b be Element of A; ::_thesis: ( (bounded_metric (A,G)) . (a,b) = 0 iff a = b )
A12: ( (bounded_metric (A,G)) . (a,b) = 0 implies a = b )
proof
assume  (bounded_metric (A,G)) . (a,b) = 0 ; ::_thesis: a = b
then A13: (G . (a,b)) / (1 + (G . (a,b))) = 0 by Def1;
 0 <= G . (a,b) by A1, Th2;
then  G . (a,b) = 0 by A13, XCMPLX_1:50;
hence  a = b by A1, PCOMPS_1:def_6; ::_thesis: verum
end;
 ( a = b implies (bounded_metric (A,G)) . (a,b) = 0 )
proof
assume  a = b ; ::_thesis: (bounded_metric (A,G)) . (a,b) = 0
then  G . (a,b) = 0 by A1, PCOMPS_1:def_6;
then  (G . (a,b)) / (1 + (G . (a,b))) = 0 ;
hence  (bounded_metric (A,G)) . (a,b) = 0 by Def1; ::_thesis: verum
end;
hence  ( (bounded_metric (A,G)) . (a,b) = 0 iff a = b ) by A12; ::_thesis: verum
end;
 for a, b being Element of A holds (bounded_metric (A,G)) . (a,b) = (bounded_metric (A,G)) . (b,a)
proof
let a, b be Element of A; ::_thesis: (bounded_metric (A,G)) . (a,b) = (bounded_metric (A,G)) . (b,a)
(G . (a,b)) / (1 + (G . (a,b))) = (G . (b,a)) / (1 + (G . (a,b))) by A1, PCOMPS_1:def_6
.= (G . (b,a)) / (1 + (G . (b,a))) by A1, PCOMPS_1:def_6
.= (bounded_metric (A,G)) . (b,a) by Def1 ;
hence  (bounded_metric (A,G)) . (a,b) = (bounded_metric (A,G)) . (b,a) by Def1; ::_thesis: verum
end;
hence  bounded_metric (A,G) is_metric_of A by A11, A2, PCOMPS_1:def_6; ::_thesis: verum
end;


theorem Th7: :: METRIC_6:7
for X being non empty MetrSpace
for x being Element of X ex S being sequence of X st rng S = {x}
proof
let X be non empty MetrSpace; ::_thesis: for x being Element of X ex S being sequence of X st rng S = {x}
let x be Element of X; ::_thesis: ex S being sequence of X st rng S = {x}
consider f being Function such that
A1: dom f = NAT and
A2: rng f = {x} by FUNCT_1:5;
reconsider f = f as sequence of X by A1, A2, FUNCT_2:2;
take  f ; ::_thesis: rng f = {x}
thus  rng f = {x} by A2; ::_thesis: verum
end;

definition
let X be non empty MetrStruct ;
let S be sequence of X;
let x be Element of X;
predS is_convergent_in_metrspace_to x means :Def2: :: METRIC_6:def 2
 for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r;
end;

:: deftheorem Def2 defines is_convergent_in_metrspace_to METRIC_6:def_2_:_
 for X being non empty MetrStruct
for S being sequence of X
for x being Element of X holds
( S is_convergent_in_metrspace_to x iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r );

definition
let X be non empty symmetric triangle MetrStruct ;
let V be Subset of X;
redefine attr V is bounded  means :Def3: :: METRIC_6:def 3
 ex r being Real ex x being Element of X st
( 0 < r & V c= Ball (x,r) );
compatibility
 ( V is bounded iff ex r being Real ex x being Element of X st
( 0 < r & V c= Ball (x,r) ) )
proof
hereby  ::_thesis: ( ex r being Real ex x being Element of X st
( 0 < r & V c= Ball (x,r) ) implies V is bounded )
assume A1: V is bounded ; ::_thesis: ex s being Element of REAL ex x being Element of X st
( 0 < s & V c= Ball (x,s) )
percases ( V <> {} or V = {} ) ;
suppose V <> {} ; ::_thesis: ex s being Element of REAL ex x being Element of X st
( 0 < s & V c= Ball (x,s) )
then consider x being Element of X such that
A2: x in V by SUBSET_1:4;
consider r being Real such that
A3: 0 < r and
A4: for x, y being Element of X st x in V & y in V holds
dist (x,y) <= r by A1, TBSP_1:def_7;
take s = 2 * r; ::_thesis: ex x being Element of X st
( 0 < s & V c= Ball (x,s) )
take x = x; ::_thesis: ( 0 < s & V c= Ball (x,s) )
thus  0 < s by A3, XREAL_1:129; ::_thesis: V c= Ball (x,s)
thus  V c= Ball (x,s) ::_thesis: verum
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in V or u in Ball (x,s) )
assume A5: u in V ; ::_thesis: u in Ball (x,s)
then reconsider v = u as Element of X ;
A6: 1 * r < s by A3, XREAL_1:68;
 dist (x,v) <= r by A4, A2, A5;
then  dist (x,v) < s by A6, XXREAL_0:2;
hence  u in Ball (x,s) by METRIC_1:11; ::_thesis: verum
end;
end;
supposeA7: V = {} ; ::_thesis: ex r being Element of REAL ex x being Element of X st
( 0 < r & V c= Ball (x,r) )
set x = the Element of X;
take r = 1 / 2; ::_thesis: ex x being Element of X st
( 0 < r & V c= Ball (x,r) )
take x = the Element of X; ::_thesis: ( 0 < r & V c= Ball (x,r) )
thus  ( 0 < r & V c= Ball (x,r) ) by A7, XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
given r being Real, x being Element of X such that A8: 0 < r and
A9: V c= Ball (x,r) ; ::_thesis: V is bounded
take  2 * r ; :: according to TBSP_1:def_7 ::_thesis: ( not 2 * r <= 0 & ( for b1, b2 being Element of the carrier of X holds
( not b1 in V or not b2 in V or dist (b1,b2) <= 2 * r ) ) )
thus  2 * r > 0 by A8, XREAL_1:129; ::_thesis: for b1, b2 being Element of the carrier of X holds
( not b1 in V or not b2 in V or dist (b1,b2) <= 2 * r )
let z, y be Element of X; ::_thesis: ( not z in V or not y in V or dist (z,y) <= 2 * r )
assume A10: z in V ; ::_thesis: ( not y in V or dist (z,y) <= 2 * r )
assume  y in V ; ::_thesis: dist (z,y) <= 2 * r
then A11: dist (x,y) < r by A9, METRIC_1:11;
 dist (x,z) < r by A9, A10, METRIC_1:11;
then A12: (dist (z,x)) + (dist (x,y)) <= r + r by A11, XREAL_1:7;
 dist (z,y) <= (dist (z,x)) + (dist (x,y)) by METRIC_1:4;
hence  dist (z,y) <= 2 * r by A12, XXREAL_0:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines bounded METRIC_6:def_3_:_
 for X being non empty symmetric triangle MetrStruct
for V being Subset of X holds
( V is bounded iff ex r being Real ex x being Element of X st
( 0 < r & V c= Ball (x,r) ) );

definition
let X be non empty MetrStruct ;
let S be sequence of X;
attrS is bounded  means :Def4: :: METRIC_6:def 4
 ex r being Real ex x being Element of X st
( 0 < r & rng S c= Ball (x,r) );
end;

:: deftheorem Def4 defines bounded METRIC_6:def_4_:_
 for X being non empty MetrStruct
for S being sequence of X holds
( S is bounded iff ex r being Real ex x being Element of X st
( 0 < r & rng S c= Ball (x,r) ) );

definition
let X be non empty MetrSpace;
let V be Subset of X;
let S be sequence of X;
predV contains_almost_all_sequence S means :Def5: :: METRIC_6:def 5
 ex m being Element of NAT st
for n being Element of NAT st m <= n holds
S . n in V;
end;

:: deftheorem Def5 defines contains_almost_all_sequence METRIC_6:def_5_:_
 for X being non empty MetrSpace
for V being Subset of X
for S being sequence of X holds
( V contains_almost_all_sequence S iff ex m being Element of NAT st
for n being Element of NAT st m <= n holds
S . n in V );

theorem Th8: :: METRIC_6:8
for X being non empty MetrSpace
for S being sequence of X holds
( S is bounded iff ex r being Real ex x being Element of X st
( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) )
proof
let X be non empty MetrSpace; ::_thesis: for S being sequence of X holds
( S is bounded iff ex r being Real ex x being Element of X st
( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) )
let S be sequence of X; ::_thesis: ( S is bounded iff ex r being Real ex x being Element of X st
( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) )
thus  ( S is bounded implies ex r being Real ex x being Element of X st
( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) ) ::_thesis: ( ex r being Real ex x being Element of X st
( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) implies S is bounded )
proof
assume  S is bounded ; ::_thesis: ex r being Real ex x being Element of X st
( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) )
then consider r being Real, x being Element of X such that
A1: 0 < r and
A2: rng S c= Ball (x,r) by Def4;
take q = r; ::_thesis: ex x being Element of X st
( 0 < q & ( for n being Element of NAT holds S . n in Ball (x,q) ) )
take y = x; ::_thesis: ( 0 < q & ( for n being Element of NAT holds S . n in Ball (y,q) ) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_S_._n_in_Ball_(y,q)
let n be Element of NAT ; ::_thesis: S . n in Ball (y,q)
 S . n in rng S by FUNCT_2:4;
hence  S . n in Ball (y,q) by A2; ::_thesis: verum
end;
hence  ( 0 < q & ( for n being Element of NAT holds S . n in Ball (y,q) ) ) by A1; ::_thesis: verum
end;
thus  ( ex r being Real ex x being Element of X st
( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) implies S is bounded ) ::_thesis: verum
proof
given r being Real, x being Element of X such that A3: 0 < r and
A4: for n being Element of NAT holds S . n in Ball (x,r) ; ::_thesis: S is bounded
 for x1 being set st x1 in rng S holds
x1 in Ball (x,r)
proof
let x1 be set ; ::_thesis: ( x1 in rng S implies x1 in Ball (x,r) )
assume  x1 in rng S ; ::_thesis: x1 in Ball (x,r)
then consider x2 being set  such that
A5: x2 in dom S and
A6: x1 = S . x2 by FUNCT_1:def_3;
 x2 in NAT by A5, FUNCT_2:def_1;
hence  x1 in Ball (x,r) by A4, A6; ::_thesis: verum
end;
then  rng S c= Ball (x,r) by TARSKI:def_3;
hence  S is bounded by A3, Def4; ::_thesis: verum
end;
end;

theorem Th9: :: METRIC_6:9
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x holds
S is convergent
proof
let X be non empty MetrSpace; ::_thesis: for x being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x holds
S is convergent
let x be Element of X; ::_thesis: for S being sequence of X st S is_convergent_in_metrspace_to x holds
S is convergent
let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x implies S is convergent )
assume A1: S is_convergent_in_metrspace_to x ; ::_thesis: S is convergent
take  x ; :: according to TBSP_1:def_2 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= dist ((S . b3),x) ) )
thus  for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= dist ((S . b3),x) ) ) by A1, Def2; ::_thesis: verum
end;

theorem Th10: :: METRIC_6:10
for X being non empty MetrSpace
for S being sequence of X st S is convergent holds
ex x being Element of X st S is_convergent_in_metrspace_to x
proof
let X be non empty MetrSpace; ::_thesis: for S being sequence of X st S is convergent holds
ex x being Element of X st S is_convergent_in_metrspace_to x
let S be sequence of X; ::_thesis: ( S is convergent implies ex x being Element of X st S is_convergent_in_metrspace_to x )
assume  S is convergent ; ::_thesis: ex x being Element of X st S is_convergent_in_metrspace_to x
then consider x being Element of X such that
A1: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r by TBSP_1:def_2;
 S is_convergent_in_metrspace_to x by A1, Def2;
hence  ex x being Element of X st S is_convergent_in_metrspace_to x ; ::_thesis: verum
end;

definition
let X be non empty MetrSpace;
let S be sequence of X;
let x be Element of X;
func dist_to_point (S,x) ->  Real_Sequence means :Def6: :: METRIC_6:def 6
 for n being Element of NAT holds it . n = dist ((S . n),x);
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = dist ((S . n),x)
proof
deffunc H1( Element of NAT ) ->  Element of REAL = dist ((S . $1),x);
consider seq being Real_Sequence such that
A1: for n being Element of NAT holds seq . n = H1(n) from SEQ_1:sch_1();
take  seq ; ::_thesis: for n being Element of NAT holds seq . n = dist ((S . n),x)
thus  for n being Element of NAT holds seq . n = dist ((S . n),x) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = dist ((S . n),x) ) & ( for n being Element of NAT holds b2 . n = dist ((S . n),x) ) holds
b1 = b2
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = dist ((S . n),x) ) & ( for n being Element of NAT holds seq2 . n = dist ((S . n),x) ) implies seq1 = seq2 )
assume that
A2: for n being Element of NAT holds seq1 . n = dist ((S . n),x) and
A3: for n being Element of NAT holds seq2 . n = dist ((S . n),x) ; ::_thesis: seq1 = seq2
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_seq2_._n
let n be Element of NAT ; ::_thesis: seq1 . n = seq2 . n
 seq1 . n = dist ((S . n),x) by A2;
hence  seq1 . n = seq2 . n by A3; ::_thesis: verum
end;
hence  seq1 = seq2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines dist_to_point METRIC_6:def_6_:_
 for X being non empty MetrSpace
for S being sequence of X
for x being Element of X
for b4 being Real_Sequence holds
( b4 = dist_to_point (S,x) iff for n being Element of NAT holds b4 . n = dist ((S . n),x) );

definition
let X be non empty MetrSpace;
let S, T be sequence of X;
func sequence_of_dist (S,T) ->  Real_Sequence means :Def7: :: METRIC_6:def 7
 for n being Element of NAT holds it . n = dist ((S . n),(T . n));
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = dist ((S . n),(T . n))
proof
deffunc H1( Element of NAT ) ->  Element of REAL = dist ((S . $1),(T . $1));
consider seq being Real_Sequence such that
A1: for n being Element of NAT holds seq . n = H1(n) from SEQ_1:sch_1();
take  seq ; ::_thesis: for n being Element of NAT holds seq . n = dist ((S . n),(T . n))
thus  for n being Element of NAT holds seq . n = dist ((S . n),(T . n)) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = dist ((S . n),(T . n)) ) & ( for n being Element of NAT holds b2 . n = dist ((S . n),(T . n)) ) holds
b1 = b2
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = dist ((S . n),(T . n)) ) & ( for n being Element of NAT holds seq2 . n = dist ((S . n),(T . n)) ) implies seq1 = seq2 )
assume that
A2: for n being Element of NAT holds seq1 . n = dist ((S . n),(T . n)) and
A3: for n being Element of NAT holds seq2 . n = dist ((S . n),(T . n)) ; ::_thesis: seq1 = seq2
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_seq2_._n
let n be Element of NAT ; ::_thesis: seq1 . n = seq2 . n
 seq1 . n = dist ((S . n),(T . n)) by A2;
hence  seq1 . n = seq2 . n by A3; ::_thesis: verum
end;
hence  seq1 = seq2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines sequence_of_dist METRIC_6:def_7_:_
 for X being non empty MetrSpace
for S, T being sequence of X
for b4 being Real_Sequence holds
( b4 = sequence_of_dist (S,T) iff for n being Element of NAT holds b4 . n = dist ((S . n),(T . n)) );

theorem Th11: :: METRIC_6:11
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x holds
lim S = x
proof
let X be non empty MetrSpace; ::_thesis: for x being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x holds
lim S = x
let x be Element of X; ::_thesis: for S being sequence of X st S is_convergent_in_metrspace_to x holds
lim S = x
let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x implies lim S = x )
assume  S is_convergent_in_metrspace_to x ; ::_thesis: lim S = x
then  ( S is convergent & ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r ) ) by Def2, Th9;
hence  lim S = x by TBSP_1:def_3; ::_thesis: verum
end;

theorem Th12: :: METRIC_6:12
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) )
proof
let X be non empty MetrSpace; ::_thesis: for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) )
let x be Element of X; ::_thesis: for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) )
let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) )
 ( S is convergent & lim S = x implies S is_convergent_in_metrspace_to x )
proof
assume  ( S is convergent & lim S = x ) ; ::_thesis: S is_convergent_in_metrspace_to x
then  for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r by TBSP_1:def_3;
hence  S is_convergent_in_metrspace_to x by Def2; ::_thesis: verum
end;
hence  ( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) ) by Th9, Th11; ::_thesis: verum
end;

theorem Th13: :: METRIC_6:13
for X being non empty MetrSpace
for S being sequence of X st S is convergent holds
ex x being Element of X st
( S is_convergent_in_metrspace_to x & lim S = x )
proof
let X be non empty MetrSpace; ::_thesis: for S being sequence of X st S is convergent holds
ex x being Element of X st
( S is_convergent_in_metrspace_to x & lim S = x )
let S be sequence of X; ::_thesis: ( S is convergent implies ex x being Element of X st
( S is_convergent_in_metrspace_to x & lim S = x ) )
assume  S is convergent ; ::_thesis: ex x being Element of X st
( S is_convergent_in_metrspace_to x & lim S = x )
then  ex x being Element of X st S is_convergent_in_metrspace_to x by Th10;
hence  ex x being Element of X st
( S is_convergent_in_metrspace_to x & lim S = x ) by Th11; ::_thesis: verum
end;

theorem Th14: :: METRIC_6:14
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )
proof
let X be non empty MetrSpace; ::_thesis: for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )
let x be Element of X; ::_thesis: for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )
let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )
A1: ( S is_convergent_in_metrspace_to x implies ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )
proof
assume A2: S is_convergent_in_metrspace_to x ; ::_thesis: ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 )
A3: for r being real number st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((dist_to_point (S,x)) . n) - 0) < r
proof
let r be real number ; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((dist_to_point (S,x)) . n) - 0) < r )
assume A4: 0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((dist_to_point (S,x)) . n) - 0) < r
reconsider r = r as Real by XREAL_0:def_1;
consider m1 being Element of NAT  such that
A5: for n being Element of NAT st m1 <= n holds
dist ((S . n),x) < r by A2, A4, Def2;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
abs (((dist_to_point (S,x)) . n) - 0) < r
let n be Element of NAT ; ::_thesis: ( k <= n implies abs (((dist_to_point (S,x)) . n) - 0) < r )
assume  k <= n ; ::_thesis: abs (((dist_to_point (S,x)) . n) - 0) < r
then  dist ((S . n),x) < r by A5;
then A6: (dist_to_point (S,x)) . n < r by Def6;
 dist ((S . n),x) = (dist_to_point (S,x)) . n by Def6;
then  0 <= (dist_to_point (S,x)) . n by METRIC_1:5;
hence  abs (((dist_to_point (S,x)) . n) - 0) < r by A6, ABSVALUE:def_1; ::_thesis: verum
end;
then  dist_to_point (S,x) is convergent by SEQ_2:def_6;
hence  ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) by A3, SEQ_2:def_7; ::_thesis: verum
end;
 ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 implies S is_convergent_in_metrspace_to x )
proof
assume A7: ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) ; ::_thesis: S is_convergent_in_metrspace_to x
 for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r
proof
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r )
assume  0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r
then consider m1 being Element of NAT  such that
A8: for n being Element of NAT st m1 <= n holds
abs (((dist_to_point (S,x)) . n) - 0) < r by A7, SEQ_2:def_7;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
dist ((S . n),x) < r
let n be Element of NAT ; ::_thesis: ( k <= n implies dist ((S . n),x) < r )
assume  k <= n ; ::_thesis: dist ((S . n),x) < r
then  abs (((dist_to_point (S,x)) . n) - 0) < r by A8;
then A9: abs (dist ((S . n),x)) < r by Def6;
 0 <= dist ((S . n),x) by METRIC_1:5;
hence  dist ((S . n),x) < r by A9, ABSVALUE:def_1; ::_thesis: verum
end;
hence  S is_convergent_in_metrspace_to x by Def2; ::_thesis: verum
end;
hence  ( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) ) by A1; ::_thesis: verum
end;

theorem Th15: :: METRIC_6:15
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x holds
for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S
proof
let X be non empty MetrSpace; ::_thesis: for x being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x holds
for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S
let x be Element of X; ::_thesis: for S being sequence of X st S is_convergent_in_metrspace_to x holds
for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S
let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x implies for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S )
assume A1: S is_convergent_in_metrspace_to x ; ::_thesis: for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S
thus  for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ::_thesis: verum
proof
let r be Real; ::_thesis: ( 0 < r implies Ball (x,r) contains_almost_all_sequence S )
assume A2: 0 < r ; ::_thesis: Ball (x,r) contains_almost_all_sequence S
 ex m being Element of NAT st
for n being Element of NAT st m <= n holds
S . n in Ball (x,r)
proof
consider m1 being Element of NAT  such that
A3: for n being Element of NAT st m1 <= n holds
dist ((S . n),x) < r by A1, A2, Def2;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
S . n in Ball (x,r)
now__::_thesis:_for_n_being_Element_of_NAT_st_k_<=_n_holds_
S_._n_in_Ball_(x,r)
let n be Element of NAT ; ::_thesis: ( k <= n implies S . n in Ball (x,r) )
assume  k <= n ; ::_thesis: S . n in Ball (x,r)
then  dist (x,(S . n)) < r by A3;
hence  S . n in Ball (x,r) by METRIC_1:11; ::_thesis: verum
end;
hence  for n being Element of NAT st k <= n holds
S . n in Ball (x,r) ; ::_thesis: verum
end;
hence  Ball (x,r) contains_almost_all_sequence S by Def5; ::_thesis: verum
end;
end;

theorem Th16: :: METRIC_6:16
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X st ( for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) holds
for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S
proof
let X be non empty MetrSpace; ::_thesis: for x being Element of X
for S being sequence of X st ( for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) holds
for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S
let x be Element of X; ::_thesis: for S being sequence of X st ( for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) holds
for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S
let S be sequence of X; ::_thesis: ( ( for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) implies for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S )
assume A1: for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ; ::_thesis: for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S
A2: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
S . n in Ball (x,r)
proof
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
S . n in Ball (x,r) )
assume  0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
S . n in Ball (x,r)
then  Ball (x,r) contains_almost_all_sequence S by A1;
hence  ex m being Element of NAT st
for n being Element of NAT st m <= n holds
S . n in Ball (x,r) by Def5; ::_thesis: verum
end;
thus  for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ::_thesis: verum
proof
let V be Subset of X; ::_thesis: ( x in V & V in Family_open_set X implies V contains_almost_all_sequence S )
assume  ( x in V & V in Family_open_set X ) ; ::_thesis: V contains_almost_all_sequence S
then consider q being Real such that
A3: 0 < q and
A4: Ball (x,q) c= V by PCOMPS_1:def_4;
consider m1 being Element of NAT  such that
A5: for n being Element of NAT st m1 <= n holds
S . n in Ball (x,q) by A2, A3;
now__::_thesis:_for_n_being_Element_of_NAT_st_m1_<=_n_holds_
S_._n_in_V
let n be Element of NAT ; ::_thesis: ( m1 <= n implies S . n in V )
assume  m1 <= n ; ::_thesis: S . n in V
then  S . n in Ball (x,q) by A5;
hence  S . n in V by A4; ::_thesis: verum
end;
hence  V contains_almost_all_sequence S by Def5; ::_thesis: verum
end;
end;

theorem Th17: :: METRIC_6:17
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X st ( for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) holds
S is_convergent_in_metrspace_to x
proof
let X be non empty MetrSpace; ::_thesis: for x being Element of X
for S being sequence of X st ( for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) holds
S is_convergent_in_metrspace_to x
let x be Element of X; ::_thesis: for S being sequence of X st ( for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) holds
S is_convergent_in_metrspace_to x
let S be sequence of X; ::_thesis: ( ( for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) implies S is_convergent_in_metrspace_to x )
A1: for r being Real st 0 < r holds
x in Ball (x,r)
proof
let r be Real; ::_thesis: ( 0 < r implies x in Ball (x,r) )
assume  0 < r ; ::_thesis: x in Ball (x,r)
then  dist (x,x) < r by METRIC_1:1;
hence  x in Ball (x,r) by METRIC_1:11; ::_thesis: verum
end;
assume A2: for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ; ::_thesis: S is_convergent_in_metrspace_to x
 for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r
proof
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r )
assume  0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r
then  x in Ball (x,r) by A1;
then  Ball (x,r) contains_almost_all_sequence S by A2, PCOMPS_1:29;
then consider m1 being Element of NAT  such that
A3: for n being Element of NAT st m1 <= n holds
S . n in Ball (x,r) by Def5;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
dist ((S . n),x) < r
let n be Element of NAT ; ::_thesis: ( k <= n implies dist ((S . n),x) < r )
assume  k <= n ; ::_thesis: dist ((S . n),x) < r
then  S . n in Ball (x,r) by A3;
hence  dist ((S . n),x) < r by METRIC_1:11; ::_thesis: verum
end;
hence  S is_convergent_in_metrspace_to x by Def2; ::_thesis: verum
end;

theorem :: METRIC_6:18
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S )
proof
let X be non empty MetrSpace; ::_thesis: for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S )
let x be Element of X; ::_thesis: for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S )
let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x iff for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S )
thus  ( S is_convergent_in_metrspace_to x implies for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) by Th15; ::_thesis: ( ( for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) implies S is_convergent_in_metrspace_to x )
thus  ( ( for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) implies S is_convergent_in_metrspace_to x ) ::_thesis: verum
proof
assume  for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ; ::_thesis: S is_convergent_in_metrspace_to x
then  for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S by Th16;
hence  S is_convergent_in_metrspace_to x by Th17; ::_thesis: verum
end;
end;

theorem :: METRIC_6:19
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S )
proof
let X be non empty MetrSpace; ::_thesis: for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S )
let x be Element of X; ::_thesis: for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S )
let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x iff for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S )
thus  ( S is_convergent_in_metrspace_to x implies for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) ::_thesis: ( ( for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) implies S is_convergent_in_metrspace_to x )
proof
assume  S is_convergent_in_metrspace_to x ; ::_thesis: for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S
then  for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S by Th15;
hence  for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S by Th16; ::_thesis: verum
end;
thus  ( ( for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) implies S is_convergent_in_metrspace_to x ) by Th17; ::_thesis: verum
end;

theorem :: METRIC_6:20
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X holds
( ( for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) iff for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) by Th15, Th16, Th17;

theorem Th21: :: METRIC_6:21
for X being non empty MetrSpace
for S, T being sequence of X st S is convergent & T is convergent holds
dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T))
proof
let X be non empty MetrSpace; ::_thesis: for S, T being sequence of X st S is convergent & T is convergent holds
dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T))
let S, T be sequence of X; ::_thesis: ( S is convergent & T is convergent implies dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T)) )
assume that
A1: S is convergent and
A2: T is convergent ; ::_thesis: dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T))
consider x being Element of X such that
A3: S is_convergent_in_metrspace_to x and
A4: lim S = x by A1, Th13;
consider y being Element of X such that
A5: T is_convergent_in_metrspace_to y and
A6: lim T = y by A2, Th13;
A7: for r being real number st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r
proof
let r be real number ; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r )
assume A8: 0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r
reconsider r = r as Real by XREAL_0:def_1;
A9: 0 < r / 2 by A8, XREAL_1:215;
then consider m1 being Element of NAT  such that
A10: for n being Element of NAT st m1 <= n holds
dist ((S . n),x) < r / 2 by A3, Def2;
consider m2 being Element of NAT  such that
A11: for n being Element of NAT st m2 <= n holds
dist ((T . n),y) < r / 2 by A5, A9, Def2;
take k = m1 + m2; ::_thesis: for n being Element of NAT st k <= n holds
abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r
let n be Element of NAT ; ::_thesis: ( k <= n implies abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r )
assume A12: k <= n ; ::_thesis: abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r
 ( abs ((dist ((S . n),(T . n))) - (dist (x,(T . n)))) <= dist ((S . n),x) & abs ((dist ((T . n),x)) - (dist (y,x))) <= dist ((T . n),y) ) by Th1;
then A13: (abs ((dist ((S . n),(T . n))) - (dist ((T . n),x)))) + (abs ((dist ((T . n),x)) - (dist (x,y)))) <= (dist ((S . n),x)) + (dist ((T . n),y)) by XREAL_1:7;
abs (((sequence_of_dist (S,T)) . n) - (dist ((lim S),(lim T)))) = abs ((dist ((S . n),(T . n))) - (dist (x,y))) by A4, A6, Def7
.= abs (((dist ((S . n),(T . n))) - (dist ((T . n),x))) + ((dist ((T . n),x)) - (dist (x,y)))) ;
then  abs (((sequence_of_dist (S,T)) . n) - (dist ((lim S),(lim T)))) <= (abs ((dist ((S . n),(T . n))) - (dist ((T . n),x)))) + (abs ((dist ((T . n),x)) - (dist (x,y)))) by COMPLEX1:56;
then A14: abs (((sequence_of_dist (S,T)) . n) - (dist ((lim S),(lim T)))) <= (dist ((S . n),x)) + (dist ((T . n),y)) by A13, XXREAL_0:2;
 m2 <= k by NAT_1:12;
then  m2 <= n by A12, XXREAL_0:2;
then A15: dist ((T . n),y) < r / 2 by A11;
 m1 <= k by NAT_1:11;
then  m1 <= n by A12, XXREAL_0:2;
then  dist ((S . n),x) < r / 2 by A10;
then  (dist ((S . n),x)) + (dist ((T . n),y)) < (r / 2) + (r / 2) by A15, XREAL_1:8;
hence  abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r by A4, A6, A14, XXREAL_0:2; ::_thesis: verum
end;
then  sequence_of_dist (S,T) is convergent by SEQ_2:def_6;
hence  dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T)) by A4, A6, A7, SEQ_2:def_7; ::_thesis: verum
end;

theorem :: METRIC_6:22
for X being non empty MetrSpace
for x, y being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y holds
x = y
proof
let X be non empty MetrSpace; ::_thesis: for x, y being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y holds
x = y
let x, y be Element of X; ::_thesis: for S being sequence of X st S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y holds
x = y
let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y implies x = y )
assume that
A1: S is_convergent_in_metrspace_to x and
A2: S is_convergent_in_metrspace_to y ; ::_thesis: x = y
A3: lim S = y by A2, Th12;
A4: for n being Nat holds (sequence_of_dist (S,S)) . n = 0
proof
let n be Nat; ::_thesis: (sequence_of_dist (S,S)) . n = 0
 n in NAT by ORDINAL1:def_12;
then (sequence_of_dist (S,S)) . n = dist ((S . n),(S . n)) by Def7
.= 0 by METRIC_1:1 ;
hence  (sequence_of_dist (S,S)) . n = 0 ; ::_thesis: verum
end;
A5: ex n being Element of NAT st (sequence_of_dist (S,S)) . n = 0
proof
take  0 ; ::_thesis: (sequence_of_dist (S,S)) . 0 = 0
thus  (sequence_of_dist (S,S)) . 0 = 0 by A4; ::_thesis: verum
end;
 ( lim S = x & S is convergent ) by A1, Th12;
then A6: dist (x,y) = lim (sequence_of_dist (S,S)) by A3, Th21;
 sequence_of_dist (S,S) is constant by A4, VALUED_0:def_18;
then  dist (x,y) = 0 by A6, A5, SEQ_4:25;
hence  x = y by METRIC_1:2; ::_thesis: verum
end;

theorem Th23: :: METRIC_6:23
for X being non empty MetrSpace
for S being sequence of X st S is constant holds
S is convergent
proof
let X be non empty MetrSpace; ::_thesis: for S being sequence of X st S is constant holds
S is convergent
let S be sequence of X; ::_thesis: ( S is constant implies S is convergent )
assume  S is constant ; ::_thesis: S is convergent
then consider x being Element of X such that
A1: for n being Nat holds S . n = x by VALUED_0:def_18;
take  x ; :: according to TBSP_1:def_2 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= dist ((S . b3),x) ) )
let r be Real; ::_thesis: ( r <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not r <= dist ((S . b2),x) ) )
assume A2: 0 < r ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not r <= dist ((S . b2),x) )
take k = 0 ; ::_thesis: for b1 being Element of NAT holds
( not k <= b1 or not r <= dist ((S . b1),x) )
now__::_thesis:_for_n_being_Element_of_NAT_st_k_<=_n_holds_
dist_((S_._n),x)_<_r
let n be Element of NAT ; ::_thesis: ( k <= n implies dist ((S . n),x) < r )
assume  k <= n ; ::_thesis: dist ((S . n),x) < r
dist ((S . n),x) = dist (x,x) by A1
.= 0 by METRIC_1:1 ;
hence  dist ((S . n),x) < r by A2; ::_thesis: verum
end;
hence  for n being Element of NAT st k <= n holds
dist ((S . n),x) < r ; ::_thesis: verum
end;

theorem :: METRIC_6:24
for X being non empty MetrSpace
for x being Element of X
for S, S1 being sequence of X st S is_convergent_in_metrspace_to x & S1 is subsequence of S holds
S1 is_convergent_in_metrspace_to x
proof
let X be non empty MetrSpace; ::_thesis: for x being Element of X
for S, S1 being sequence of X st S is_convergent_in_metrspace_to x & S1 is subsequence of S holds
S1 is_convergent_in_metrspace_to x
let x be Element of X; ::_thesis: for S, S1 being sequence of X st S is_convergent_in_metrspace_to x & S1 is subsequence of S holds
S1 is_convergent_in_metrspace_to x
let S, S1 be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x & S1 is subsequence of S implies S1 is_convergent_in_metrspace_to x )
assume that
A1: S is_convergent_in_metrspace_to x and
A2: S1 is subsequence of S ; ::_thesis: S1 is_convergent_in_metrspace_to x
consider Nseq being increasing sequence of NAT such that
A3: S1 = S * Nseq by A2, VALUED_0:def_17;
 for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S1 . n),x) < r
proof
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S1 . n),x) < r )
assume  0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S1 . n),x) < r
then consider m1 being Element of NAT  such that
A4: for n being Element of NAT st m1 <= n holds
dist ((S . n),x) < r by A1, Def2;
take m = m1; ::_thesis: for n being Element of NAT st m <= n holds
dist ((S1 . n),x) < r
 for n being Element of NAT st m <= n holds
dist ((S1 . n),x) < r
proof
let n be Element of NAT ; ::_thesis: ( m <= n implies dist ((S1 . n),x) < r )
assume A5: m <= n ; ::_thesis: dist ((S1 . n),x) < r
 dom S = NAT by FUNCT_2:def_1;
then  ( dom Nseq = NAT & Nseq . n in dom S ) by FUNCT_2:def_1;
then  n in dom (S * Nseq) by FUNCT_1:11;
then A6: S1 . n = S . (Nseq . n) by A3, FUNCT_1:12;
 n <= Nseq . n by SEQM_3:14;
then  m1 <= Nseq . n by A5, XXREAL_0:2;
hence  dist ((S1 . n),x) < r by A4, A6; ::_thesis: verum
end;
hence  for n being Element of NAT st m <= n holds
dist ((S1 . n),x) < r ; ::_thesis: verum
end;
hence  S1 is_convergent_in_metrspace_to x by Def2; ::_thesis: verum
end;

theorem :: METRIC_6:25
for X being non empty MetrSpace
for S, S1 being sequence of X st S is Cauchy & S1 is subsequence of S holds
S1 is Cauchy
proof
let X be non empty MetrSpace; ::_thesis: for S, S1 being sequence of X st S is Cauchy & S1 is subsequence of S holds
S1 is Cauchy
let S, S1 be sequence of X; ::_thesis: ( S is Cauchy & S1 is subsequence of S implies S1 is Cauchy )
assume that
A1: S is Cauchy and
A2: S1 is subsequence of S ; ::_thesis: S1 is Cauchy
consider Nseq being increasing sequence of NAT such that
A3: S1 = S * Nseq by A2, VALUED_0:def_17;
 for r being Real st 0 < r holds
ex m being Element of NAT st
for n, k being Element of NAT st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r
proof
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n, k being Element of NAT st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r )
assume  0 < r ; ::_thesis: ex m being Element of NAT st
for n, k being Element of NAT st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r
then consider m1 being Element of NAT  such that
A4: for n, k being Element of NAT st m1 <= n & m1 <= k holds
dist ((S . n),(S . k)) < r by A1, TBSP_1:def_4;
take m = m1; ::_thesis: for n, k being Element of NAT st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r
 for n, k being Element of NAT st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r
proof
let n, k be Element of NAT ; ::_thesis: ( m <= n & m <= k implies dist ((S1 . n),(S1 . k)) < r )
assume that
A5: m <= n and
A6: m <= k ; ::_thesis: dist ((S1 . n),(S1 . k)) < r
 k <= Nseq . k by SEQM_3:14;
then A7: m1 <= Nseq . k by A6, XXREAL_0:2;
 dom S = NAT by FUNCT_2:def_1;
then  ( dom Nseq = NAT & Nseq . k in dom S ) by FUNCT_2:def_1;
then  k in dom (S * Nseq) by FUNCT_1:11;
then A8: S1 . k = S . (Nseq . k) by A3, FUNCT_1:12;
 dom S = NAT by FUNCT_2:def_1;
then  ( dom Nseq = NAT & Nseq . n in dom S ) by FUNCT_2:def_1;
then  n in dom (S * Nseq) by FUNCT_1:11;
then A9: S1 . n = S . (Nseq . n) by A3, FUNCT_1:12;
 n <= Nseq . n by SEQM_3:14;
then  m1 <= Nseq . n by A5, XXREAL_0:2;
hence  dist ((S1 . n),(S1 . k)) < r by A4, A9, A7, A8; ::_thesis: verum
end;
hence  for n, k being Element of NAT st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r ; ::_thesis: verum
end;
hence  S1 is Cauchy by TBSP_1:def_4; ::_thesis: verum
end;

theorem :: METRIC_6:26
for X being non empty MetrSpace
for S being sequence of X st S is constant holds
S is Cauchy by Th23, TBSP_1:5;

theorem :: METRIC_6:27
for X being non empty MetrSpace
for S being sequence of X st S is convergent holds
S is bounded
proof
let X be non empty MetrSpace; ::_thesis: for S being sequence of X st S is convergent holds
S is bounded
let S be sequence of X; ::_thesis: ( S is convergent implies S is bounded )
assume  S is convergent ; ::_thesis: S is bounded
then consider x being Element of X such that
A1: S is_convergent_in_metrspace_to x and
 lim S = x by Th13;
 dist_to_point (S,x) is convergent by A1, Th14;
then  dist_to_point (S,x) is bounded by SEQ_2:13;
then consider r being real number  such that
A2: 0 < r and
A3: for n being Element of NAT holds abs ((dist_to_point (S,x)) . n) < r by SEQ_2:3;
reconsider r = r as Real by XREAL_0:def_1;
 for n being Element of NAT holds S . n in Ball (x,r)
proof
let n be Element of NAT ; ::_thesis: S . n in Ball (x,r)
A4: (dist_to_point (S,x)) . n = dist ((S . n),x) by Def6;
then  0 <= (dist_to_point (S,x)) . n by METRIC_1:5;
then  abs ((dist_to_point (S,x)) . n) = (dist_to_point (S,x)) . n by ABSVALUE:def_1;
then  dist ((S . n),x) < r by A3, A4;
hence  S . n in Ball (x,r) by METRIC_1:11; ::_thesis: verum
end;
hence  S is bounded by A2, Th8; ::_thesis: verum
end;

theorem Th28: :: METRIC_6:28
for X being non empty MetrSpace
for S being sequence of X st S is Cauchy holds
S is bounded
proof
let X be non empty MetrSpace; ::_thesis: for S being sequence of X st S is Cauchy holds
S is bounded
let S be sequence of X; ::_thesis: ( S is Cauchy implies S is bounded )
assume A1: S is Cauchy ; ::_thesis: S is bounded
now__::_thesis:_ex_r_being_Element_of_NAT_st_
(_0_<_r_&_ex_m_being_Element_of_NAT_st_
for_n,_k_being_Element_of_NAT_st_m_<=_n_&_m_<=_k_holds_
dist_((S_._n),(S_._k))_<_r_)
take r = 1; ::_thesis: ( 0 < r & ex m being Element of NAT st
for n, k being Element of NAT st m <= n & m <= k holds
dist ((S . n),(S . k)) < r )
thus  0 < r ; ::_thesis: ex m being Element of NAT st
for n, k being Element of NAT st m <= n & m <= k holds
dist ((S . n),(S . k)) < r
consider m1 being Element of NAT  such that
A2: for n, k being Element of NAT st m1 <= n & m1 <= k holds
dist ((S . n),(S . k)) < r by A1, TBSP_1:def_4;
take m = m1; ::_thesis: for n, k being Element of NAT st m <= n & m <= k holds
dist ((S . n),(S . k)) < r
thus  for n, k being Element of NAT st m <= n & m <= k holds
dist ((S . n),(S . k)) < r by A2; ::_thesis: verum
end;
then consider r2 being Real, m1 being Element of NAT  such that
A3: 0 < r2 and
A4: for n, k being Element of NAT st m1 <= n & m1 <= k holds
dist ((S . n),(S . k)) < r2 ;
consider r1 being real number  such that
A5: 0 < r1 and
A6: for m2 being Element of NAT st m2 <= m1 holds
abs ((dist_to_point (S,(S . m1))) . m2) < r1 by SEQ_2:4;
A7: for m being Element of NAT st m <= m1 holds
dist ((S . m),(S . m1)) < r1
proof
let m be Element of NAT ; ::_thesis: ( m <= m1 implies dist ((S . m),(S . m1)) < r1 )
assume A8: m <= m1 ; ::_thesis: dist ((S . m),(S . m1)) < r1
A9: (dist_to_point (S,(S . m1))) . m = dist ((S . m),(S . m1)) by Def6;
then  0 <= (dist_to_point (S,(S . m1))) . m by METRIC_1:5;
then  abs ((dist_to_point (S,(S . m1))) . m) = dist ((S . m),(S . m1)) by A9, ABSVALUE:def_1;
hence  dist ((S . m),(S . m1)) < r1 by A6, A8; ::_thesis: verum
end;
 ex r being Real ex x being Element of X st
( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) )
proof
reconsider r = r1 + r2 as Real ;
take  r ; ::_thesis: ex x being Element of X st
( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) )
take x = S . m1; ::_thesis: ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) )
 for n being Element of NAT holds S . n in Ball (x,r)
proof
let n be Element of NAT ; ::_thesis: S . n in Ball (x,r)
now__::_thesis:_S_._n_in_Ball_(x,r)
percases ( n <= m1 or m1 <= n ) ;
supposeA10: n <= m1 ; ::_thesis: S . n in Ball (x,r)
A11: r1 < r by A3, XREAL_1:29;
 dist ((S . n),(S . m1)) < r1 by A7, A10;
then  dist ((S . n),x) < r by A11, XXREAL_0:2;
hence  S . n in Ball (x,r) by METRIC_1:11; ::_thesis: verum
end;
supposeA12: m1 <= n ; ::_thesis: S . n in Ball (x,r)
A13: r2 < r by A5, XREAL_1:29;
 dist ((S . n),(S . m1)) < r2 by A4, A12;
then  dist ((S . n),x) < r by A13, XXREAL_0:2;
hence  S . n in Ball (x,r) by METRIC_1:11; ::_thesis: verum
end;
end;
end;
hence  S . n in Ball (x,r) ; ::_thesis: verum
end;
hence  ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) by A3, A5; ::_thesis: verum
end;
hence  S is bounded by Th8; ::_thesis: verum
end;

registration
let M be non empty MetrSpace;
cluster Function-like constant V30( NAT , the carrier of M)  ->  convergent for Element of bool [:NAT, the carrier of M:];
coherence
 for b1 being sequence of M st b1 is constant holds
b1 is convergent by Th23;
cluster Function-like V30( NAT , the carrier of M) Cauchy  ->  bounded for Element of bool [:NAT, the carrier of M:];
coherence
 for b1 being sequence of M st b1 is Cauchy holds
b1 is bounded by Th28;
end;

registration
let M be non empty MetrSpace;
cluster non empty Relation-like NAT -defined the carrier of M -valued Function-like constant V29( NAT ) V30( NAT , the carrier of M) convergent Cauchy bounded for Element of bool [:NAT, the carrier of M:];
existence
 ex b1 being sequence of M st
( b1 is constant & b1 is convergent & b1 is Cauchy & b1 is bounded )
proof
set x = the Element of M;
consider S being sequence of M such that
A1: rng S = { the Element of M} by Th7;
take  S ; ::_thesis: ( S is constant & S is convergent & S is Cauchy & S is bounded )
thus A2: S is constant by A1, FUNCT_2:111; ::_thesis: ( S is convergent & S is Cauchy & S is bounded )
hence  S is convergent ; ::_thesis: ( S is Cauchy & S is bounded )
thus  S is Cauchy by A2; ::_thesis: S is bounded
thus  S is bounded by A2; ::_thesis: verum
end;
end;

theorem :: METRIC_6:29
for X being non empty Reflexive symmetric triangle MetrStruct
for V being bounded Subset of X
for x being Element of X ex r being Real st
( 0 < r & V c= Ball (x,r) )
proof
let X be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for V being bounded Subset of X
for x being Element of X ex r being Real st
( 0 < r & V c= Ball (x,r) )
let V be bounded Subset of X; ::_thesis: for x being Element of X ex r being Real st
( 0 < r & V c= Ball (x,r) )
let y be Element of X; ::_thesis: ex r being Real st
( 0 < r & V c= Ball (y,r) )
consider r being Real, x being Element of X such that
A1: 0 < r and
A2: V c= Ball (x,r) by Def3;
take s = r + (dist (x,y)); ::_thesis: ( 0 < s & V c= Ball (y,s) )
 dist (x,y) >= 0 by METRIC_1:5;
then  s >= r + 0 by XREAL_1:7;
hence  0 < s by A1; ::_thesis: V c= Ball (y,s)
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in V or e in Ball (y,s) )
assume A3: e in V ; ::_thesis: e in Ball (y,s)
then reconsider e = e as Element of X ;
 e in Ball (x,r) by A3, A2;
then  dist (e,x) < r by METRIC_1:11;
then A4: (dist (e,x)) + (dist (x,y)) < r + (dist (x,y)) by XREAL_1:8;
 dist (e,y) <= (dist (e,x)) + (dist (x,y)) by METRIC_1:4;
then  dist (e,y) < r + (dist (x,y)) by A4, XXREAL_0:2;
then  e in Ball (y,s) by METRIC_1:11;
hence  e in Ball (y,s) ; ::_thesis: verum
end;