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

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