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

hence |.seq.| is bounded by A1, A3, SEQ_2:3; :: thesis: verum

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

|.(seq . 0).| < r
by A2;
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.| . n = |.(seq . n).| by VALUED_1:18;

hence |.(|.seq.| . n).| < r by A2; :: thesis: verum

hence |.seq.| is bounded by A1, A3, SEQ_2:3; :: thesis: verum