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

for x being object st x in A /\ (dom f) holds

f . x <= a

hence f | A is bounded by A7; :: thesis: verum

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

then A7:
f | A is bounded_below
by RFUNCT_1:71;
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;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

for x being object st x in A /\ (dom f) holds

f . x <= a

proof

then
f | A is bounded_above
by RFUNCT_1:70;
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;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

hence f | A is bounded by A7; :: thesis: verum