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 Nat st
for n, k being Nat st m <= n & m <= k holds
dist ((S . n),(S . k)) < r )

take r = 1; :: thesis: ( 0 < r & ex m being Nat st
for n, k being Nat st m <= n & m <= k holds
dist ((S . n),(S . k)) < r )
thus 0 < r ; :: thesis: ex m being Nat st
for n, k being Nat st m <= n & m <= k holds
dist ((S . n),(S . k)) < r
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: for n, k being Nat st m <= n & m <= k holds
dist ((S . n),(S . k)) < r
thus for n, k being 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 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: ( 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 |.((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 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 Nat holds S . n in Ball (x,r) ) )
take x = S . m1; :: thesis: ( 0 < r & ( for n being Nat holds S . n in Ball (x,r) ) )
for n being Nat holds S . n in Ball (x,r)

proof

let n be Nat; :: thesis: S . n in Ball (x,r)

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

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

suppose A10: 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;

suppose A12: 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 Nat holds S . n in Ball (x,r) ) ) by A3, A5; :: thesis: verum

end;

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