let X, Y be non empty set ; :: thesis: for f being PartFunc of X,REAL st f | X is bounded_below & Y c= X holds

(f | Y) | Y is bounded_below

let f be PartFunc of X,REAL; :: thesis: ( f | X is bounded_below & Y c= X implies (f | Y) | Y is bounded_below )

assume f | X is bounded_below ; :: thesis: ( not Y c= X or (f | Y) | Y is bounded_below )

then consider a being Real such that

A1: for x being object st x in X /\ (dom f) holds

f . x >= a by RFUNCT_1:71;

assume A2: Y c= X ; :: thesis: (f | Y) | Y is bounded_below

for x being object st x in Y /\ (dom (f | Y)) holds

(f | Y) . x >= a

(f | Y) | Y is bounded_below

let f be PartFunc of X,REAL; :: thesis: ( f | X is bounded_below & Y c= X implies (f | Y) | Y is bounded_below )

assume f | X is bounded_below ; :: thesis: ( not Y c= X or (f | Y) | Y is bounded_below )

then consider a being Real such that

A1: for x being object st x in X /\ (dom f) holds

f . x >= a by RFUNCT_1:71;

assume A2: Y c= X ; :: thesis: (f | Y) | Y is bounded_below

for x being object st x in Y /\ (dom (f | Y)) holds

(f | Y) . x >= a

proof

hence
(f | Y) | Y is bounded_below
by RFUNCT_1:71; :: thesis: verum
let x be object ; :: thesis: ( x in Y /\ (dom (f | Y)) implies (f | Y) . x >= a )

A3: (dom f) /\ Y c= (dom f) /\ X by A2, XBOOLE_1:26;

assume x in Y /\ (dom (f | Y)) ; :: thesis: (f | Y) . x >= a

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 (f | Y) . x >= a 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: (f | Y) . x >= a

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 (f | Y) . x >= a by A4, FUNCT_1:47; :: thesis: verum