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 A1: f | X is bounded_above ; :: thesis: rng f is bounded_above
consider a being real number such that
A2: for x1 being set st x1 in X /\ (dom f) holds
f . x1 <= a by A1, RFUNCT_1:87;
A3: X /\ (dom f) = dom f by XBOOLE_1:28;
for y being real number st y in rng f holds
y <= a

proof

let y be real number ; :: thesis: ( y in rng f implies y <= a )
assume y in rng f ; :: thesis: y <= a
then consider s being set such that
A4: ( s in dom f & y = f . s ) by FUNCT_1:def 5;
thus y <= a by A2, A3, A4; :: thesis: verum

end;

hence rng f is bounded_above by SEQ_4:def 1; :: thesis: verum