let seq be Complex_Sequence; :: thesis: ( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable )
( Partial_Sums |.seq.| is bounded_above iff |.seq.| is summable ) ;
hence ( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable ) ; :: thesis: verum