for X being ComplexUnitarySpace
for seq being sequence of X
for n being Nat holds Sum (seq,(n + 1)) = (Sum (seq,n)) + (seq . (n + 1)) by BHSP_4:def 1;