theorem :: CLVECT_3:21

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