:: deftheorem defines Sum AFINSQ_2:def 9 :
for F being XFinSequence holds Sum F = addcomplex "**" F;