let X, Y be non empty set ; :: thesis: for f being PartFunc of X,REAL st f | X is bounded_above & Y c= X holds
(f | Y) | Y is bounded_above
let f be PartFunc of X,REAL; :: thesis: ( f | X is bounded_above & Y c= X implies (f | Y) | Y is bounded_above )
assume f | X is bounded_above ; :: thesis: ( not Y c= X or (f | Y) | Y is bounded_above )
then consider a being Real such that
A1: for x being object st x in X /\ (dom f) holds
a >= f . x by RFUNCT_1:70;
assume A2: Y c= X ; :: thesis: (f | Y) | Y is bounded_above
for x being object st x in Y /\ (dom (f | Y)) holds
a >= (f | Y) . x

proof

let x be object ; :: thesis: ( x in Y /\ (dom (f | Y)) implies a >= (f | Y) . x )
A3: (dom f) /\ Y c= (dom f) /\ X by A2, XBOOLE_1:26;
assume x in Y /\ (dom (f | Y)) ; :: thesis: a >= (f | Y) . x
then A4: x in dom (f | Y) by XBOOLE_0:def 4;
then x in (dom f) /\ Y by RELAT_1:61;
then a >= f . x by A1, A3;
hence a >= (f | Y) . x by A4, FUNCT_1:47; :: thesis: verum

end;

hence (f | Y) | Y is bounded_above by RFUNCT_1:70; :: thesis: verum