for X being ComplexNormSpace
for s, s1 being sequence of X st ( for n being Nat holds s1 . n = s . 0 ) holds
Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1