let s be Complex_Sequence; :: thesis: ( s is bounded iff ex r being Real st
( 0 < r & ( for n being Nat holds |.(s . n).| < r ) ) )
thus ( s is bounded implies ex r being Real st
( 0 < r & ( for n being Nat holds |.(s . n).| < r ) ) ) :: thesis: ( ex r being Real st
( 0 < r & ( for n being Nat holds |.(s . n).| < r ) ) implies s is bounded )

proof

assume s is bounded ; :: thesis: ex r being Real st
( 0 < r & ( for n being Nat holds |.(s . n).| < r ) )
then consider r being Real such that
A1: for n being Nat holds |.(s . n).| < r ;
take r ; :: thesis: ( 0 < r & ( for n being Nat holds |.(s . n).| < r ) )

now :: thesis: for n being Nat holds 0 < r

let n be Nat; :: thesis: 0 < r
0 <= |.(s . n).| by COMPLEX1:46;
hence 0 < r by A1; :: thesis: verum

end;

hence ( 0 < r & ( for n being Nat holds |.(s . n).| < r ) ) by A1; :: thesis: verum

end;

thus ( ex r being Real st
( 0 < r & ( for n being Nat holds |.(s . n).| < r ) ) implies s is bounded ) ; :: thesis: verum