theorem Th22: :: COMSEQ_2:33
for s being convergent Complex_Sequence st lim s <> 0c holds
ex n being Nat st
for m being Nat st n <= m holds
|.(lim s).| / 2 < |.(s . m).|