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

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

hence
seq is bounded
by COMSEQ_2:def 4; :: thesis: verum
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;|.seq.| . n = |.(seq . n).| by VALUED_1:18;

then |.(|.seq.| . n).| = |.(seq . n).| ;

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