let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL st f is without-infty & f is without+infty holds
f is PartFunc of X,REAL
let f be PartFunc of X,ExtREAL; :: thesis: ( f is without-infty & f is without+infty implies f is PartFunc of X,REAL )
assume ( f is without-infty & f is without+infty ) ; :: thesis: f is PartFunc of X,REAL
then ( not -infty in rng f & not +infty in rng f ) by MESFUNC5:def 3, MESFUNC5:def 4;
then rng f c= REAL by XXREAL_0:14;
hence f is PartFunc of X,REAL by RELSET_1:6; :: thesis: verum