:: deftheorem DEF12 defines summable MEASUR11:def 10 :
for X being non empty set
for F being FinSequence of Funcs (X,ExtREAL) holds
( F is summable iff ( F is without_+infty-valued or F is without_-infty-valued ) );