theorem :: CLVECT_3:20

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