:: deftheorem defines Sum BHSP_4:def 5 :
for X being RealUnitarySpace
for seq being sequence of X
for n, m being Nat holds Sum (seq,n,m) = (Sum (seq,n)) - (Sum (seq,m));