let X be non empty set ; :: thesis: for f being without-infty without+infty Function of X,ExtREAL holds f is Function of X,REAL
let f be without-infty without+infty Function of X,ExtREAL; :: thesis: f is Function of X,REAL
A1: dom f = X by FUNCT_2:def 1;

now :: thesis: for x being object st x in X holds
f . x in REAL

let x be object ; :: thesis: ( x in X implies f . x in REAL )
assume x in X ; :: thesis: f . x in REAL
then ( f . x in ExtREAL & f . x > -infty & f . x < +infty ) by FUNCT_2:5, MESFUNC5:def 5, MESFUNC5:def 6;
hence f . x in REAL by XXREAL_0:14; :: thesis: verum

end;

hence f is Function of X,REAL by A1, FUNCT_2:3; :: thesis: verum