theorem :: COMSEQ_3:45

for seq being Complex_Sequence
for r being Real st r > 0 & ex m being Nat st
for n being Nat st n >= m holds
|.(seq . n).| >= r & |.seq.| is convergent holds
lim |.seq.| <> 0