:: deftheorem DEF11 defines without_-infty-valued MEASUR11:def 9 :
for X being set
for F being FinSequence of Funcs (X,ExtREAL) holds
( F is without_-infty-valued iff for n being Nat st n in dom F holds
F . n is without-infty );