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