for X being RealUnitarySpace
for seq, seq1 being sequence of X st ( for n being Nat holds seq1 . n = seq . 0 ) holds
Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1