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
A2: 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
reconsider y = y as R_eal by A3;
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;
A7: - +infty < y by A5, A6, EXTREAL2:58;
A8: -infty < y by A7, XXREAL_3:def 3;
A9: y < +infty by A5, A6, EXTREAL2:58;
thus y in REAL by A8, A9, XXREAL_0:14; :: thesis: verum

end;

thus rng f is Subset of REAL by A2; :: thesis: verum