theorem :: CSSPACE2:11

for seq being Complex_Sequence st seq is summable & ( for n being Nat holds
( (Re seq) . n >= 0 & (Im seq) . n = 0 ) ) holds
|.(Sum seq).| = Sum |.seq.| by Lm7;