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

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 5;
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:16;
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 Def14;
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 ) )
A10: 0 + 0 < r1 + r2 by A3, A5;
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

per cases ( n <= m1 or m1 <= n ) ;

suppose n <= m1 ; :: thesis: S . n in Ball x,r

then A11: dist (S . n),(S . m1) < r1 by A7;
r1 < r by A3, XREAL_1:31;
then dist (S . n),x < r by A11, XXREAL_0:2;
hence S . n in Ball x,r by METRIC_1:12; :: thesis: verum

end;

suppose m1 <= n ; :: thesis: S . n in Ball x,r

then A12: dist (S . n),(S . m1) < r2 by A4;
r2 < r by A5, XREAL_1:31;
then dist (S . n),x < r by A12, XXREAL_0:2;
hence S . n in Ball x,r by METRIC_1:12; :: 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 A10; :: thesis: verum

end;

hence S is bounded by Th20; :: thesis: verum