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 Th28;
dist_to_point (S,x) is convergent by A1, Th29;
then dist_to_point (S,x) is bounded by SEQ_2:27;
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:15;
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 Def14;
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:12; :: thesis: verum

end;

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