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 )

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

( 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

thus
( ex r being Real st
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 ) )

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

end;( 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 ) )

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

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