for k being Nat
for seq being Complex_Sequence holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k)