let s be Complex_Sequence; :: thesis: ( s is convergent implies s is bounded )
assume s is convergent ; :: thesis: s is bounded
then consider g being Complex such that
A1: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - g).| < p ;
1 in NAT ;
then reconsider j = 1 as Element of REAL by NUMBERS:19;
consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
|.((s . m) - g).| < j by A1;

now :: thesis: ex R being set st
( 0 < R & ( for m being Nat st n1 <= m holds
|.(s . m).| < R ) )

take R = |.g.| + 1; :: thesis: ( 0 < R & ( for m being Nat st n1 <= m holds
|.(s . m).| < R ) )
0 + 0 < R by COMPLEX1:46, XREAL_1:8;
hence 0 < R ; :: thesis: for m being Nat st n1 <= m holds
|.(s . m).| < R
let m be Nat; :: thesis: ( n1 <= m implies |.(s . m).| < R )
A3: (|.(s . m).| - |.g.|) + |.g.| = |.(s . m).| ;
assume n1 <= m ; :: thesis: |.(s . m).| < R
then A4: |.((s . m) - g).| < 1 by A2;
|.(s . m).| - |.g.| <= |.((s . m) - g).| by COMPLEX1:59;
then |.(s . m).| - |.g.| < 1 by A4, XXREAL_0:2;
hence |.(s . m).| < R by A3, XREAL_1:6; :: thesis: verum

end;

then consider R1 being Real such that
A5: 0 < R1 and
A6: for m being Nat st n1 <= m holds
|.(s . m).| < R1 ;
consider R2 being Real such that
A7: 0 < R2 and
A8: for m being Nat st m <= n1 holds
|.(s . m).| < R2 by Th2;
reconsider R = R1 + R2 as Real ;
take R ; :: according to COMSEQ_2:def 4 :: thesis: for n being Nat holds |.(s . n).| < R
let m be Nat; :: thesis: |.(s . m).| < R
A9: R2 + 0 < R by A5, XREAL_1:8;

A10: now :: thesis: ( m <= n1 implies |.(s . m).| < R )

assume m <= n1 ; :: thesis: |.(s . m).| < R
then |.(s . m).| < R2 by A8;
hence |.(s . m).| < R by A9, XXREAL_0:2; :: thesis: verum

end;

A11: R1 + 0 < R by A7, XREAL_1:8;

now :: thesis: ( n1 <= m implies |.(s . m).| < R )

assume n1 <= m ; :: thesis: |.(s . m).| < R
then |.(s . m).| < R1 by A6;
hence |.(s . m).| < R by A11, XXREAL_0:2; :: thesis: verum

end;

hence |.(s . m).| < R by A10; :: thesis: verum