:: deftheorem defines Sum RVSUM_1:def 11 :
for F being FinSequence of COMPLEX holds Sum F = addcomplex $$ F;