theorem Th19: :: CLVECT_3:19

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