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 such that
A2: 0 < r and
A3: for n being Nat holds |.((dist_to_point (S,x)) . n).| < r by SEQ_2:3;
reconsider r = r as Real ;
for n being Nat holds S . n in Ball (x,r)
proof
let n be 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 |.((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