let X be non empty set ; :: thesis: for f being PartFunc of X,REAL st f | X is bounded_above holds
rng f is bounded_above
let f be PartFunc of X,REAL; :: thesis: ( f | X is bounded_above implies rng f is bounded_above )
assume f | X is bounded_above ; :: thesis: rng f is bounded_above
then consider a being real number such that
A1: for x1 being set st x1 in X /\ (dom f) holds
f . x1 <= a by RFUNCT_1:70;
A2: X /\ (dom f) = dom f by XBOOLE_1:28;
a is UpperBound of rng f

proof

let y be ext-real number ; :: 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 set st
( s in dom f & y = f . s ) by FUNCT_1:def 3;
hence y <= a by A1, A2; :: thesis: verum

end;

hence rng f is bounded_above by XXREAL_2:def 10; :: thesis: verum