:: deftheorem defines Sum CLVECT_3:def 4 :
for X being ComplexUnitarySpace
for seq being sequence of X
for n, m being Nat holds Sum (seq,n,m) = (Sum (seq,n)) - (Sum (seq,m));