let X be non empty MetrSpace; :: thesis:
let S be sequence of X; :: thesis:
assume A1: S is Cauchy ; :: thesis:

now :: thesis:

take r = 1; :: thesis:
thus 0 < r ; :: thesis:
consider m1 being Nat such that
A2: for n, k being Nat st m1 <= n & m1 <= k holds
dist ((S . n),(S . k)) < r by A1;
take m = m1; :: thesis:
thus for n, k being Nat st m <= n & m <= k holds
dist ((S . n),(S . k)) < r by A2; :: thesis:

end;

then consider r2 being Real, m1 being Nat such that
A3: 0 < r2 and
A4: for n, k being Nat st m1 <= n & m1 <= k holds
dist ((S . n),(S . k)) < r2 ;
consider r1 being Real such that
A5: 0 < r1 and
A6: for m2 being Nat st m2 <= m1 holds
|.((dist_to_point (S,(S . m1))) . m2).| < r1 by SEQ_2:4;
A7: for m being Nat st m <= m1 holds
dist ((S . m),(S . m1)) < r1

proof

let m be Nat; :: thesis:
assume A8: m <= m1 ; :: thesis:
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 |.((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:

end;

ex r being Real ex x being Element of X st
( 0 < r & ( for n being Nat holds S . n in Ball (x,r) ) )

proof

reconsider r = r1 + r2 as Real ;
take r ; :: thesis:
take x = S . m1; :: thesis:
for n being Nat holds S . n in Ball (x,r)

proof

let n be Nat; :: thesis:

now :: thesis:

per cases ;

suppose A10: n <= m1 ; :: thesis:

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:

end;

suppose A12: m1 <= n ; :: thesis:

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:

end;

end;

end;

hence S . n in Ball (x,r) ; :: thesis:

end;

hence ( 0 < r & ( for n being Nat holds S . n in Ball (x,r) ) ) by A3, A5; :: thesis:

end;

hence S is bounded by Th8; :: thesis: