theorem Th16: :: BHSP_4:16

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