let seq be Complex_Sequence; :: thesis: ( seq is absolutely_summable implies |.(Sum seq).| <= Sum |.seq.| )

A1: for k being Nat holds |.(Partial_Sums seq).| . k <= (Partial_Sums |.seq.|) . k

then reconsider Pseq = Partial_Sums seq as convergent Complex_Sequence ;

A3: |.(Sum seq).| = |.(lim (Partial_Sums seq)).| by COMSEQ_3:def 7

.= lim |.(Partial_Sums seq).| by A2, SEQ_2:27 ;

( |.Pseq.| is convergent & Partial_Sums |.seq.| is convergent ) by A2, SERIES_1:def 2;

then lim |.(Partial_Sums seq).| <= lim (Partial_Sums |.seq.|) by A1, SEQ_2:18;

hence |.(Sum seq).| <= Sum |.seq.| by A3, SERIES_1:def 3; :: thesis: verum

A1: for k being Nat holds |.(Partial_Sums seq).| . k <= (Partial_Sums |.seq.|) . k

proof

assume A2:
seq is absolutely_summable
; :: thesis: |.(Sum seq).| <= Sum |.seq.|
let k be 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;|.((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

then reconsider Pseq = Partial_Sums seq as convergent Complex_Sequence ;

A3: |.(Sum seq).| = |.(lim (Partial_Sums seq)).| by COMSEQ_3:def 7

.= lim |.(Partial_Sums seq).| by A2, SEQ_2:27 ;

( |.Pseq.| is convergent & Partial_Sums |.seq.| is convergent ) by A2, SERIES_1:def 2;

then lim |.(Partial_Sums seq).| <= lim (Partial_Sums |.seq.|) by A1, SEQ_2:18;

hence |.(Sum seq).| <= Sum |.seq.| by A3, SERIES_1:def 3; :: thesis: verum