let A be non empty 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 real-bounded by A1, FCONT_1:29, RCOMP_1:10;
then consider a being Real such that
A3: a is UpperBound of f .: A by XXREAL_2:def 10;
A4: for r being Real st r in f .: A holds
r <= a by A3, XXREAL_2:def 1;
consider b being Real such that
A5: b is LowerBound of f .: A by A2, XXREAL_2:def 9;
A6: for r being Real st r in f .: A holds
b <= r by A5, XXREAL_2:def 2;
for x being object st x in A /\ (dom f) holds
b <= f . x

proof

let x be object ; :: 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 6;
hence b <= f . x by A6; :: thesis: verum

end;

then A7: f | A is bounded_below by RFUNCT_1:71;
for x being object st x in A /\ (dom f) holds
f . x <= a

proof

let x be object ; :: 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 6;
hence f . x <= a by A4; :: thesis: verum

end;

then f | A is bounded_above by RFUNCT_1:70;
hence f | A is bounded by A7; :: thesis: verum