let seq be sequence of X; :: thesis: ( seq is convergent implies seq is bounded )
assume seq is convergent ; :: thesis: seq is bounded
then consider g being Point of X such that
A1: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((seq . n) - g).|| < r by BHSP_2:9;
consider m1 being Nat such that
A2: for n being Nat st n >= m1 holds
||.((seq . n) - g).|| < 1 by A1;

A3: now :: thesis: ex p being set st
( p > 0 & ( for n being Nat st n >= m1 holds
||.(seq . n).|| < p ) )

take p = ||.g.|| + 1; :: thesis: ( p > 0 & ( for n being Nat st n >= m1 holds
||.(seq . n).|| < p ) )
0 + 0 < p by BHSP_1:28, XREAL_1:8;
hence p > 0 ; :: thesis: for n being Nat st n >= m1 holds
||.(seq . n).|| < p
let n be Nat; :: thesis: ( n >= m1 implies ||.(seq . n).|| < p )
assume n >= m1 ; :: thesis: ||.(seq . n).|| < p
then A4: ||.((seq . n) - g).|| < 1 by A2;
||.(seq . n).|| - ||.g.|| <= ||.((seq . n) - g).|| by BHSP_1:32;
then ||.(seq . n).|| - ||.g.|| < 1 by A4, XXREAL_0:2;
hence ||.(seq . n).|| < p by XREAL_1:19; :: thesis: verum

end;

now :: thesis: ex M being set st
( M > 0 & ( for n being Nat holds ||.(seq . n).|| <= M ) )

reconsider m1 = m1 as Nat ;
consider M2 being Real such that
A5: M2 > 0 and
A6: for n being Nat st n <= m1 holds
||.(seq . n).|| < M2 by Th8;
consider M1 being Real such that
A7: M1 > 0 and
A8: for n being Nat st n >= m1 holds
||.(seq . n).|| < M1 by A3;
take M = M1 + M2; :: thesis: ( M > 0 & ( for n being Nat holds ||.(seq . n).|| <= M ) )
thus M > 0 by A7, A5; :: thesis: for n being Nat holds ||.(seq . n).|| <= M
let n be Nat; :: thesis: ||.(seq . n).|| <= M
A9: M > 0 + M2 by A7, XREAL_1:8;

A10: now :: thesis: ( n <= m1 implies ||.(seq . n).|| <= M )

assume n <= m1 ; :: thesis: ||.(seq . n).|| <= M
then ||.(seq . n).|| < M2 by A6;
hence ||.(seq . n).|| <= M by A9, XXREAL_0:2; :: thesis: verum

end;

A11: M > M1 + 0 by A5, XREAL_1:8;

now :: thesis: ( n >= m1 implies ||.(seq . n).|| <= M )

assume n >= m1 ; :: thesis: ||.(seq . n).|| <= M
then ||.(seq . n).|| < M1 by A8;
hence ||.(seq . n).|| <= M by A11, XXREAL_0:2; :: thesis: verum

end;

hence ||.(seq . n).|| <= M by A10; :: thesis: verum

end;

hence seq is bounded ; :: thesis: verum