let seq be Complex_Sequence; :: thesis: ( seq is bounded implies |.seq.| is bounded )
A1: 0 <= |.(seq . 0 ).| by COMPLEX1:132;
assume seq is bounded ; :: thesis: |.seq.| is bounded
then consider r being Real such that
A2: for n being Element of NAT holds |.(seq . n).| < r by COMSEQ_2:def 3;
A3: for n being Element of NAT holds abs (|.seq.| . n) < r

proof

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

end;

|.(seq . 0 ).| < r by A2;
hence |.seq.| is bounded by A1, A3, SEQ_2:15; :: thesis: verum