let seq be sequence of X; :: thesis:
assume seq is convergent ; :: thesis:
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:

take p = ||.g.|| + 1; :: thesis:
0 + 0 < p by BHSP_1:28, XREAL_1:8;
hence p > 0 ; :: thesis:
let n be Nat; :: thesis:
assume n >= m1 ; :: thesis:
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:

end;

now :: thesis:

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:
thus M > 0 by A7, A5; :: thesis:
let n be Nat; :: thesis:
A9: M > 0 + M2 by A7, XREAL_1:8;

A10: now :: thesis:

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

end;

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

now :: thesis:

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

end;

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

end;

hence seq is bounded ; :: thesis: