let A be closed-interval Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st A c= dom f & f | A is continuous holds
f | A is bounded
let f be PartFunc of REAL ,REAL ; :: thesis: ( A c= dom f & f | A is continuous implies f | A is bounded )
assume Z: A c= dom f ; :: thesis: ( not f | A is continuous or f | A is bounded )
assume A1: f | A is continuous ; :: thesis: f | A is bounded
f .: A is bounded by A1, Z, FCONT_1:30, RCOMP_1:28;
then A2: ( f .: A is bounded_above & f .: A is bounded_below ) ;
then consider a being real number such that
A3: for r being real number st r in f .: A holds
r <= a by SEQ_4:def 1;
consider b being real number such that
A4: for r being real number st r in f .: A holds
b <= r by A2, SEQ_4:def 2;
for x being set st x in A /\ (dom f) holds
f . x <= a

proof

let x be set ; :: thesis: ( x in A /\ (dom f) implies f . x <= a )
assume x in A /\ (dom f) ; :: thesis: f . x <= a
then ( x in A & x in dom f ) by XBOOLE_0:def 4;
then f . x in f .: A by FUNCT_1:def 12;
hence f . x <= a by A3; :: thesis: verum

end;

then A5: f | A is bounded_above by RFUNCT_1:87;
for x being set st x in A /\ (dom f) holds
b <= f . x

proof

let x be set ; :: thesis: ( x in A /\ (dom f) implies b <= f . x )
assume x in A /\ (dom f) ; :: thesis: b <= f . x
then ( x in A & x in dom f ) by XBOOLE_0:def 4;
then f . x in f .: A by FUNCT_1:def 12;
hence b <= f . x by A4; :: thesis: verum

end;

then f | A is bounded_below by RFUNCT_1:88;
hence f | A is bounded by A5; :: thesis: verum