theorem Th17: :: BHSP_4:17

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