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

(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

hence
(f | Y) | Y is bounded_above
by RFUNCT_1:70; :: thesis: verum
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;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