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

proof

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

end;

hence f | X is bounded_above by RFUNCT_1:70; :: thesis: verum