let A be closed-interval Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st f | A is bounded holds
(f || A) | A is bounded
let f be PartFunc of REAL ,REAL ; :: thesis: ( f | A is bounded implies (f || A) | A is bounded )
assume f | A is bounded ; :: thesis: (f || A) | A is bounded
then ( (f || A) | A is bounded_above & (f || A) | A is bounded_below ) by Th7, Th8;
hence (f || A) | A is bounded ; :: thesis: verum