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;
A4: ( UB < +infty & -infty < LB ) by A2, A3, XXREAL_0:9, XXREAL_0:12;

now

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

end;

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