theorem Th16: :: CLVECT_3:16

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