theorem Th17: :: CLVECT_3:17

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