theorem Th17: :: MESFUN11:17

for X being non empty set
for r being negative Real
for f being Function of X,ExtREAL holds
( f is without+infty iff r (#) f is without-infty )