let N be Nat; :: thesis: for seq being Real_Sequence of N st seq is convergent holds
seq is bounded
let seq be Real_Sequence of N; :: thesis: ( seq is convergent implies seq is bounded )
assume seq is convergent ; :: thesis: seq is bounded
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: ex r being set st
( 0 < r & ( for m being Nat st n1 <= m holds
|.(seq . m).| < r ) )

take r = |.g.| + 1; :: thesis: ( 0 < r & ( for m being Nat st n1 <= m holds
|.(seq . m).| < r ) )
thus 0 < r ; :: thesis: for m being Nat st n1 <= m holds
|.(seq . m).| < r
let m be Nat; :: thesis: ( n1 <= m implies |.(seq . m).| < r )
A4: (|.(seq . m).| - |.g.|) + |.g.| = |.(seq . m).| ;
assume n1 <= m ; :: thesis: |.(seq . m).| < r
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: verum

end;

now :: thesis: ex r being set st
( 0 < r & ( for m being Nat holds |.(seq . m).| < r ) )

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: ( 0 < r & ( for m being Nat holds |.(seq . m).| < r ) )
thus 0 < r by A8, A6; :: thesis: for m being Nat holds |.(seq . m).| < r
let m be Nat; :: thesis: |.(seq . m).| < r
A10: 0 + r2 < r by A8, XREAL_1:8;

A11: now :: thesis: ( m <= n1 implies |.(seq . m).| < r )

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

end;

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

now :: thesis: ( n1 <= m implies |.(seq . m).| < r )

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

end;

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

end;

hence seq is bounded ; :: thesis: verum