:: deftheorem defines Sum CLVECT_3:def 5 :
for Cseq being Complex_Sequence
for n being Nat holds Sum (Cseq,n) = (Partial_Sums Cseq) . n;