for rseq1 being Real_Sequence
for seq being Complex_Sequence st |.seq.| is non-increasing & ( for n being Nat holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) holds
( seq is absolutely_summable iff rseq1 is summable )