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 ;
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 ;
consider b being Real such that
A5: b is LowerBound of f .: A by ;
A6: for r being Real st r in f .: A holds
b <= r by ;
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