theorem Th19: :: BHSP_4:19

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))