let A be closed-interval Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st f | A is bounded_above holds
(f || A) | A is bounded_above
let f be PartFunc of REAL ,REAL ; :: thesis: ( f | A is bounded_above implies (f || A) | A is bounded_above )
assume f | A is bounded_above ; :: thesis: (f || A) | A is bounded_above
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:87;
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 )
assume A2: x in A /\ (dom (f || A)) ; :: thesis: (f || A) . x <= r
A3: dom (f | A) = (dom f) /\ A by RELAT_1:90;
then A4: A /\ (dom (f || A)) = (dom f) /\ A by XBOOLE_1:28;
( x in A /\ (dom f) & x in dom (f | A) ) by A2, A3, XBOOLE_1:28;
then (f || A) . x = f . x by FUNCT_1:70;
hence (f || A) . x <= r by A1, A2, A4; :: thesis: verum

end;

hence (f || A) | A is bounded_above by RFUNCT_1:87; :: thesis: verum