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 such that
0 < r and
A1: for n being Nat holds |.(|.seq.| . n).| < r by SEQ_2:3;
reconsider r = r as Real ;
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;
then |.(|.seq.| . n).| = |.(seq . n).| ;
hence |.(seq . n).| < r by A1; :: thesis: verum

end;

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