:: deftheorem defines Sum CLVECT_3:def 6 :
for Cseq being Complex_Sequence
for n, m being Nat holds Sum (Cseq,n,m) = (Sum (Cseq,n)) - (Sum (Cseq,m));