let rseq1 be Real_Sequence; :: thesis: for seq being Complex_Sequence st ( for n being Nat holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is absolutely_summable
let seq be Complex_Sequence; :: thesis: ( ( for n being Nat holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is absolutely_summable )
assume A1: ( ( for n being Nat holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 ) ; :: thesis: seq is absolutely_summable
for n being Nat holds |.seq.| . n >= 0 by Lm3;
hence |.seq.| is summable by A1, SERIES_1:28; :: according to COMSEQ_3:def 9 :: thesis: verum