let seq be Complex_Sequence; :: thesis: ( seq is absolutely_summable implies |.(Sum seq).| <= Sum |.seq.| )
assume A1: seq is absolutely_summable ; :: thesis: |.(Sum seq).| <= Sum |.seq.|
then A2: seq is summable ;
then A3: Partial_Sums seq is convergent ;
reconsider Pseq = Partial_Sums seq as convergent Complex_Sequence by A2;
A4: ( |.Pseq.| is convergent & |.Pseq.| = |.(Partial_Sums seq).| ) ;
A5: |.(Sum seq).| = |.(lim (Partial_Sums seq)).| by COMSEQ_3:def 8
.= lim |.(Partial_Sums seq).| by A3, COMSEQ_2:11 ;
|.seq.| is summable by A1;
then A6: Partial_Sums |.seq.| is convergent by SERIES_1:def 2;
for k being Element of NAT holds |.(Partial_Sums seq).| . k <= (Partial_Sums |.seq.|) . k

proof

let k be Element of NAT ; :: thesis: |.(Partial_Sums seq).| . k <= (Partial_Sums |.seq.|) . k
|.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k by COMSEQ_3:30;
hence |.(Partial_Sums seq).| . k <= (Partial_Sums |.seq.|) . k by VALUED_1:18; :: thesis: verum

end;

then lim |.(Partial_Sums seq).| <= lim (Partial_Sums |.seq.|) by A4, A6, SEQ_2:32;
hence |.(Sum seq).| <= Sum |.seq.| by A5, SERIES_1:def 3; :: thesis: verum