let seq be Complex_Sequence; :: thesis: ( |.seq.| is bounded implies seq is bounded )
assume |.seq.| is bounded ; :: thesis: seq is bounded
then consider r being real number such that
0 < r and
A1: for n being Element of NAT holds abs (|.seq.| . n) < r by SEQ_2:3;
reconsider r = r as Real by XREAL_0:def 1;
for n being Element of NAT holds |.(seq . n).| < r

proof

let n be Element of NAT ; :: thesis: |.(seq . n).| < r
|.seq.| . n = |.(seq . n).| by VALUED_1:18;
then abs (|.seq.| . n) = |.(seq . n).| ;
hence |.(seq . n).| < r by A1; :: thesis: verum

end;

hence seq is bounded by COMSEQ_2:def 3; :: thesis: verum