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 and
A4: y = f . x by A2, FUNCT_1:def 3;
reconsider x = x as Element of X by A3;
A5: |.(f . x).| < +infty by A1, A3, Def1;
then - +infty < y by A4, EXTREAL2:10;
then A6: -infty < y by XXREAL_3:def 3;
y < +infty by A4, A5, EXTREAL2:10;
hence y in REAL by A6, XXREAL_0:14; :: thesis: verum

end;

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