let N be Nat; :: thesis:
let seq be Real_Sequence of N; :: thesis:
assume seq is convergent ; :: thesis:
then consider g being Point of (TOP-REAL N) such that
A1: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < r ;
consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
|.((seq . m) - g).| < 1 by A1;

A3: now :: thesis:

take r = |.g.| + 1; :: thesis:
thus 0 < r ; :: thesis:
let m be Nat; :: thesis:
A4: (|.(seq . m).| - |.g.|) + |.g.| = |.(seq . m).| ;
assume n1 <= m ; :: thesis:
then A5: |.((seq . m) - g).| < 1 by A2;
|.(seq . m).| - |.g.| <= |.((seq . m) - g).| by Th32;
then |.(seq . m).| - |.g.| < 1 by A5, XXREAL_0:2;
hence |.(seq . m).| < r by A4, XREAL_1:6; :: thesis:

end;

now :: thesis:

consider r2 being Real such that
A6: 0 < r2 and
A7: for m being Nat st m <= n1 holds
|.(seq . m).| < r2 by Th35;
consider r1 being Real such that
A8: 0 < r1 and
A9: for m being Nat st n1 <= m holds
|.(seq . m).| < r1 by A3;
take r = r1 + r2; :: thesis:
thus 0 < r by A8, A6; :: thesis:
let m be Nat; :: thesis:
A10: 0 + r2 < r by A8, XREAL_1:8;

A11: now :: thesis:

assume m <= n1 ; :: thesis:
then |.(seq . m).| < r2 by A7;
hence |.(seq . m).| < r by A10, XXREAL_0:2; :: thesis:

end;

A12: r1 + 0 < r by A6, XREAL_1:8;

now :: thesis:

assume n1 <= m ; :: thesis:
then |.(seq . m).| < r1 by A9;
hence |.(seq . m).| < r by A12, XXREAL_0:2; :: thesis:

end;

hence |.(seq . m).| < r by A11; :: thesis:

end;

hence seq is bounded ; :: thesis: