theorem :: COMSEQ_3:76

for seq being Complex_Sequence st ( for n being Nat holds seq . n <> 0c ) & ex m being Nat st
for n being Nat st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 holds
not seq is absolutely_summable