theorem :: COMSEQ_3:75

for rseq1 being Real_Sequence
for seq being Complex_Sequence st ( for n being Nat holds
( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is absolutely_summable