let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL st f is real-valued holds
rng f is Subset of REAL
let f be PartFunc of X,ExtREAL ; :: thesis: ( f is real-valued implies rng f is Subset of REAL )
assume A1: f is real-valued ; :: thesis: rng f is Subset of REAL
rng f c= REAL

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in REAL )
assume A2: y in rng f ; :: thesis: y in REAL
then reconsider y = y as R_eal ;
consider x being set such that
A3: ( x in dom f & y = f . x ) by A2, FUNCT_1:def 5;
reconsider x = x as Element of X by A3;
|.(f . x).| < +infty by A1, A3, Def1;
then ( - +infty < y & y < +infty ) by A3, EXTREAL2:58;
then ( -infty < y & y < +infty ) by XXREAL_3:def 3;
hence y in REAL by XXREAL_0:14; :: thesis: verum

end;

hence rng f is Subset of REAL ; :: thesis: verum