let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL st rng f is bounded holds
f is real-valued
let f be PartFunc of X,ExtREAL ; :: thesis: ( rng f is bounded implies f is real-valued )
assume A1: rng f is bounded ; :: thesis: f is real-valued
then rng f is bounded_above by XXREAL_2:def 11;
then consider UB being UpperBound of rng f such that
A2: UB in REAL by SUPINF_1:def 11;
rng f is bounded_below by A1, XXREAL_2:def 11;
then consider LB being LowerBound of rng f such that
A3: LB in REAL by SUPINF_1:def 12;

now

let x be Element of X; :: thesis: ( x in dom f implies |.(f . x).| < +infty )
assume A4: x in dom f ; :: thesis: |.(f . x).| < +infty
then LB <= f . x by FUNCT_1:12, XXREAL_2:def 2;
then -infty < f . x by A3, XXREAL_0:2, XXREAL_0:12;
then A5: - +infty < f . x by XXREAL_3:23;
f . x <= UB by A4, FUNCT_1:12, XXREAL_2:def 1;
then f . x < +infty by A2, XXREAL_0:2, XXREAL_0:9;
hence |.(f . x).| < +infty by A5, EXTREAL2:59; :: thesis: verum

end;

hence f is real-valued by MESFUNC2:def 1; :: thesis: verum