for n being Nat
for X being RealUnitarySpace
for seq being sequence of X holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))