theorem :: COMSEQ_3:70

for rseq1 being Real_Sequence
for seq being Complex_Sequence st ( for n being Nat holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Nat st
for n being Nat st m <= n holds
rseq1 . n >= 1 holds
not |.seq.| is summable