let seq be Complex_Sequence; :: thesis: ( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable )
for n being Element of NAT holds 0 <= |.seq.| . n by Lm3;
then ( Partial_Sums |.seq.| is bounded_above iff |.seq.| is summable ) by SERIES_1:20;
hence ( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable ) by Def11; :: thesis: verum