let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st f | A is bounded_below holds
(f || A) | A is bounded_below
let f be PartFunc of REAL,REAL; :: thesis: ( f | A is bounded_below implies (f || A) | A is bounded_below )
assume f | A is bounded_below ; :: thesis: (f || A) | A is bounded_below
then consider r being real number such that
A1: for x being set st x in A /\ (dom f) holds
f . x >= r by RFUNCT_1:71;
for x being set st x in A /\ (dom (f || A)) holds
(f || A) . x >= r

proof

let x be set ; :: thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x >= r )
dom (f | A) = (dom f) /\ A by RELAT_1:61;
then A2: A /\ (dom (f || A)) = (dom f) /\ A by XBOOLE_1:28;
assume A3: x in A /\ (dom (f || A)) ; :: thesis: (f || A) . x >= r
then x in dom (f | A) by XBOOLE_1:28;
then (f || A) . x = f . x by FUNCT_1:47;
hence (f || A) . x >= r by A1, A3, A2; :: thesis: verum

end;

hence (f || A) | A is bounded_below by RFUNCT_1:71; :: thesis: verum