theorem Th8: :: COMSEQ_2:8

for s being Complex_Sequence holds
( s is bounded iff ex r being Real st
( 0 < r & ( for n being Nat holds |.(s . n).| < r ) ) )