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 A3: y in rng f ; :: thesis: y in REAL
then reconsider y = y as R_eal ;
consider x being set such that
A4: x in dom f and
A5: y = f . x by A3, FUNCT_1:def 5;
reconsider x = x as Element of X by A4;
A6: |.(f . x).| < +infty by A1, A4, Def1;
then - +infty < y by A5, EXTREAL2:58;
then A8: -infty < y by XXREAL_3:def 3;
y < +infty by A5, A6, EXTREAL2:58;
hence y in REAL by A8, XXREAL_0:14; :: thesis: verum

end;

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