:: deftheorem defines summable MESFUNC9:def 2 :
for s being ext-real-valued Function holds
( s is summable iff Partial_Sums s is convergent );