theorem Th3: :: MESFUN14:3

for X being non empty set
for f being PartFunc of X,ExtREAL st f is without-infty & f is without+infty holds
f is PartFunc of X,REAL