let s be Complex_Sequence; :: thesis: ( s is bounded iff ex r being Real st
( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) )
thus ( s is bounded implies ex r being Real st
( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) ) :: thesis: ( ex r being Real st
( 0 < r & ( for n being Element of 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 Element of NAT holds |.(s . n).| < r ) )
then consider r being Real such that
A1: for n being Element of NAT holds |.(s . n).| < r by Def3;
take r ; :: thesis: ( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) )

now

let n be Element of NAT ; :: thesis: 0 < r
0 <= |.(s . n).| by COMPLEX1:132;
hence 0 < r by A1; :: thesis: verum

end;

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

end;

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