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

proof

let y be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not y in rng f or y <= a )
assume y in rng f ; :: thesis: y <= a
then ex s being object st
( s in dom f & y = f . s ) by FUNCT_1:def 3;
hence y <= a by A1; :: thesis: verum

end;

hence rng f is bounded_above ; :: thesis: verum