:: deftheorem DEF10 defines without_+infty-valued MEASUR11:def 8 :
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 );