let f be real-valued Function; :: thesis: ( rng f is bounded_above implies f is bounded_above )
set X = dom f;
assume rng f is bounded_above ; :: thesis: f is bounded_above
then consider a being Real such that
A1: a is UpperBound of rng f ;
AA: f | (dom f) = f ;
for x1 being object st x1 in (dom f) /\ (dom f) holds
f . x1 <= a

proof

let x1 be object ; :: thesis: ( x1 in (dom f) /\ (dom f) implies f . x1 <= a )
assume x1 in (dom f) /\ (dom f) ; :: thesis: f . x1 <= a
then f . x1 in rng f by FUNCT_1:def 3;
hence f . x1 <= a by A1, XXREAL_2:def 1; :: thesis: verum

end;

hence f is bounded_above by AA, RFUNCT_1:70; :: thesis: verum