:: deftheorem defines Sum RVSUM_1:def 12 :
for F being FinSequence of REAL holds Sum F = addreal $$ F;