:: deftheorem defines Sum SERIES_1:def 6 :
for s being Real_Sequence
for n, m being Nat holds Sum (s,n,m) = (Sum (s,n)) - (Sum (s,m));