let seq be Complex_Sequence; :: thesis: ( seq is summable & ( for n being Nat holds

( (Re seq) . n >= 0 & (Im seq) . n = 0 ) ) implies |.(Sum seq).| = Sum |.seq.| )

assume that

A1: seq is summable and

A2: for n being Nat holds

( (Re seq) . n >= 0 & (Im seq) . n = 0 ) ; :: thesis: |.(Sum seq).| = Sum |.seq.|

for x being object st x in NAT holds

|.(Partial_Sums seq).| . x = (Partial_Sums |.seq.|) . x by A2, Lm4;

then |.(Partial_Sums seq).| = Partial_Sums |.seq.| by FUNCT_2:12;

then lim |.(Partial_Sums seq).| = Sum |.seq.| by SERIES_1:def 3;

then |.(lim (Partial_Sums seq)).| = Sum |.seq.| by A1, SEQ_2:27;

hence |.(Sum seq).| = Sum |.seq.| by COMSEQ_3:def 7; :: thesis: verum

( (Re seq) . n >= 0 & (Im seq) . n = 0 ) ) implies |.(Sum seq).| = Sum |.seq.| )

assume that

A1: seq is summable and

A2: for n being Nat holds

( (Re seq) . n >= 0 & (Im seq) . n = 0 ) ; :: thesis: |.(Sum seq).| = Sum |.seq.|

for x being object st x in NAT holds

|.(Partial_Sums seq).| . x = (Partial_Sums |.seq.|) . x by A2, Lm4;

then |.(Partial_Sums seq).| = Partial_Sums |.seq.| by FUNCT_2:12;

then lim |.(Partial_Sums seq).| = Sum |.seq.| by SERIES_1:def 3;

then |.(lim (Partial_Sums seq)).| = Sum |.seq.| by A1, SEQ_2:27;

hence |.(Sum seq).| = Sum |.seq.| by COMSEQ_3:def 7; :: thesis: verum