let X be non empty MetrSpace; :: thesis:
let S be sequence of X; :: thesis:
thus ( S is bounded implies ex r being Real ex x being Element of X st
( 0 < r & ( for n being Nat holds S . n in Ball (x,r) ) ) ) :: thesis:

proof

assume S is bounded ; :: thesis:
then consider r being Real, x being Element of X such that
A1: 0 < r and
A2: rng S c= Ball (x,r) ;
take q = r; :: thesis:
take y = x; :: thesis:

now :: thesis:

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
then S . n in rng S by FUNCT_2:4;
hence S . n in Ball (y,q) by A2; :: thesis:

end;

hence ( 0 < q & ( for n being Nat holds S . n in Ball (y,q) ) ) by A1; :: thesis:

end;

thus ( ex r being Real ex x being Element of X st
( 0 < r & ( for n being Nat holds S . n in Ball (x,r) ) ) implies S is bounded ) :: thesis:

proof

given r being Real, x being Element of X such that A3: 0 < r and
A4: for n being Nat holds S . n in Ball (x,r) ; :: thesis:
reconsider r = r as Real ;
for x1 being object st x1 in rng S holds
x1 in Ball (x,r)

proof

let x1 be object ; :: thesis:
assume x1 in rng S ; :: thesis:
then consider x2 being object such that
A5: x2 in dom S and
A6: x1 = S . x2 by FUNCT_1:def 3;
x2 in NAT by A5, FUNCT_2:def 1;
hence x1 in Ball (x,r) by A4, A6; :: thesis:

end;

then rng S c= Ball (x,r) ;
hence S is bounded by A3; :: thesis:

end;