:: deftheorem defines bounded COMSEQ_2:def 4 :
for s being Complex_Sequence holds
( s is bounded iff ex r being Real st
for n being Nat holds |.(s . n).| < r );