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