let seq be Complex_Sequence; :: thesis: ( seq is bounded implies |.seq.| is bounded )
A1: 0 <= |.(seq . 0).| by COMPLEX1:46;
assume seq is bounded ; :: thesis: |.seq.| is bounded
then consider r being Real such that
A2: for n being Nat holds |.(seq . n).| < r by COMSEQ_2:def 4;
A3: for n being Nat holds |.(|.seq.| . n).| < r
proof
let n be Nat; :: thesis: |.(|.seq.| . n).| < r
|.seq.| . n = |.(seq . n).| by VALUED_1:18;
hence |.(|.seq.| . n).| < r by A2; :: thesis: verum
end;
|.(seq . 0).| < r by A2;
hence |.seq.| is bounded by A1, A3, SEQ_2:3; :: thesis: verum