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 Element of COMPLEX such that
A1: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p by Def4;
consider n1 being Element of NAT such that
A2: for m being Element of NAT st n1 <= m holds
|.((s . m) - g).| < 1 by A1;

now

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

end;

then consider R1 being real number such that
A5: 0 < R1 and
A6: for m being Element of NAT st n1 <= m holds
|.(s . m).| < R1 ;
consider R2 being Real such that
A7: 0 < R2 and
A8: for m being Element of NAT st m <= n1 holds
|.(s . m).| < R2 by Th2;
take R = R1 + R2; :: according to COMSEQ_2:def 3 :: thesis: for n being Element of NAT holds |.(s . n).| < R
A9: R1 + 0 < R by A7, XREAL_1:10;
A10: R2 + 0 < R by A5, XREAL_1:10;
let m be Element of NAT ; :: thesis: |.(s . m).| < R

A11: now

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

end;

now

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

end;

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