theorem :: CSSPACE2:8

for seq being Complex_Sequence
for n being Nat st ( for i being Nat holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) holds
|.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n by Lm4;