for seq being Complex_Sequence holds
( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable )