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