let seq be Real_Sequence; :: thesis: ( seq is convergent implies seq is bounded )
assume seq is convergent ; :: thesis: seq is bounded
then consider g being Real such that
A1: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p ;
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 ) )
0 + 0 < r by COMPLEX1:46, XREAL_1:8;
hence 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 )
assume n1 <= m ; :: thesis: |.(seq . m).| < r
then A4: |.((seq . m) - g).| < 1 by A2;
|.(seq . m).| - |.g.| <= |.((seq . m) - g).| by COMPLEX1:59;
then A5: |.(seq . m).| - |.g.| < 1 by A4, XXREAL_0:2;
(|.(seq . m).| - |.g.|) + |.g.| = |.(seq . m).| ;
hence |.(seq . m).| < r by A5, XREAL_1:6; :: thesis: verum

end;

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

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

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

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

end;

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

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

end;

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

end;

hence seq is bounded by Th3; :: thesis: verum