theorem :: BHSP_4:22

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