:: deftheorem defines Sum MESFUNC9:def 3 :
for s being ext-real-valued Function holds Sum s = lim (Partial_Sums s);