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 A1: A c= dom f ; :: thesis: ( not f | A is continuous or f | A is bounded )
assume f | A is continuous ; :: thesis: f | A is bounded
then A2: f .: A is bounded by A1, FCONT_1:30, RCOMP_1:28;
then consider a being real number such that
B3: a is UpperBound of f .: A by XXREAL_2:def 10;
A3: for r being real number st r in f .: A holds
r <= a by B3, XXREAL_2:def 1;
consider b being real number such that
B4: b is LowerBound of f .: A by A2, XXREAL_2:def 9;
A4: for r being real number st r in f .: A holds
b <= r by B4, XXREAL_2:def 2;
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 A5: f | A is bounded_below by RFUNCT_1:88;
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 f | A is bounded_above by RFUNCT_1:87;
hence f | A is bounded by A5; :: thesis: verum