let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL st f is V171() & f is V172() holds
f is PartFunc of X,REAL
let f be PartFunc of X,ExtREAL; :: thesis: ( f is V171() & f is V172() implies f is PartFunc of X,REAL )
assume ( f is V171() & f is V172() ) ; :: 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