:: deftheorem defines SUM SUPINF_2:def 12 :
for F being sequence of ExtREAL holds SUM F = sup (rng (Ser F));