let T be non empty TopSpace; :: thesis: ( ( for f being RealMap of T st f is continuous holds
f is bounded ) iff for f being RealMap of T st f is continuous holds
f is with_max )
set cT = the carrier of T;

hereby :: thesis: ( ( for f being RealMap of T st f is continuous holds
f is with_max ) implies for f being RealMap of T st f is continuous holds
f is bounded )

assume A1: for f being RealMap of T st f is continuous holds
f is bounded ; :: thesis: for f being RealMap of T st f is continuous holds
f is with_max
let f be RealMap of T; :: thesis: ( f is continuous implies f is with_max )
assume A2: f is continuous ; :: thesis: f is with_max
set fcT = f .: the carrier of T;
f is bounded by A1, A2;
then A3: f .: the carrier of T is bounded_above by MEASURE6:def 15;
set b = upper_bound (f .: the carrier of T);
set bf = (upper_bound (f .: the carrier of T)) + (- f);
- f is continuous by A2, Th55;
then A4: (upper_bound (f .: the carrier of T)) + (- f) is continuous by Th56;
reconsider bf9 = (upper_bound (f .: the carrier of T)) + (- f) as Function of the carrier of T,REAL ;
reconsider f9 = f as Function of the carrier of T,REAL ;
set g = Inv ((upper_bound (f .: the carrier of T)) + (- f));
set gcT = (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T;
assume not f is with_max ; :: thesis: contradiction
then A5: not f .: the carrier of T is right_end by MEASURE6:def 16;
then A6: not upper_bound (f .: the carrier of T) in f .: the carrier of T by A3, MEASURE6:def 8;

now

assume 0 in rng ((upper_bound (f .: the carrier of T)) + (- f)) ; :: thesis: contradiction
then consider x being set such that
A7: x in dom ((upper_bound (f .: the carrier of T)) + (- f)) and
A8: ((upper_bound (f .: the carrier of T)) + (- f)) . x = 0 by FUNCT_1:def 5;
reconsider x = x as Element of the carrier of T by A7;
bf9 . x = (upper_bound (f .: the carrier of T)) + ((- f9) . x) by VALUED_1:2
.= (upper_bound (f .: the carrier of T)) + (- (f . x)) by VALUED_1:8
.= (upper_bound (f .: the carrier of T)) - (f . x) ;
hence contradiction by A6, A8, FUNCT_2:43; :: thesis: verum

end;

then A9: Inv ((upper_bound (f .: the carrier of T)) + (- f)) is continuous by A4, Th57;

now

Inv ((upper_bound (f .: the carrier of T)) + (- f)) is bounded by A1, A9;
then (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T is bounded_above by MEASURE6:def 15;
then consider p being real number such that
B10: p is UpperBound of (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T by XXREAL_2:def 10;
A10: for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p by B10, XXREAL_2:def 1;

per cases ( p <= 0 or p > 0 ) ;

suppose A11: p <= 0 ; :: thesis: ex a19 being real number st
( a19 > 0 & ( for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= a19 ) )

reconsider a19 = 1 as real number ;
take a19 = a19; :: thesis: ( a19 > 0 & ( for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= a19 ) )
thus a19 > 0 ; :: thesis: for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= a19
let r be real number ; :: thesis: ( r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T implies r <= a19 )
assume r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T ; :: thesis: r <= a19
hence r <= a19 by A10, A11; :: thesis: verum

end;

suppose A12: p > 0 ; :: thesis: ex p being real number st
( p > 0 & ( for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p ) )

take p = p; :: thesis: ( p > 0 & ( for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p ) )
thus p > 0 by A12; :: thesis: for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p
thus for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p by A10; :: thesis: verum

end;

end;

end;

then consider p being real number such that
A13: p > 0 and
A14: for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p ;
consider r being real number such that
A15: r in f .: the carrier of T and
A16: (upper_bound (f .: the carrier of T)) - (1 / p) < r by A3, A13, SEQ_4:def 4;
consider x being set such that
A17: x in the carrier of T and
x in the carrier of T and
A18: r = f . x by A15, FUNCT_2:115;
reconsider x = x as Element of T by A17;
A19: f . x <= upper_bound (f .: the carrier of T) by A3, A15, A18, SEQ_4:def 4;
f . x <> upper_bound (f .: the carrier of T) by A3, A5, A15, A18, MEASURE6:def 8;
then (f . x) + 0 < upper_bound (f .: the carrier of T) by A19, XXREAL_0:1;
then A20: (upper_bound (f .: the carrier of T)) - (f . x) > 0 by XREAL_1:22;
(Inv ((upper_bound (f .: the carrier of T)) + (- f))) . x = (bf9 . x) " by VALUED_1:10
.= ((upper_bound (f .: the carrier of T)) + ((- f9) . x)) " by VALUED_1:2
.= 1 / ((upper_bound (f .: the carrier of T)) + ((- f9) . x))
.= 1 / ((upper_bound (f .: the carrier of T)) + (- (f . x))) by VALUED_1:8
.= 1 / ((upper_bound (f .: the carrier of T)) - (f . x)) ;
then 1 / ((upper_bound (f .: the carrier of T)) - (f . x)) <= p by A14, FUNCT_2:43;
then 1 <= p * ((upper_bound (f .: the carrier of T)) - (f . x)) by A20, XREAL_1:83;
then 1 / p <= (upper_bound (f .: the carrier of T)) - (f . x) by A13, XREAL_1:81;
then (f . x) + (1 / p) <= upper_bound (f .: the carrier of T) by XREAL_1:21;
hence contradiction by A16, A18, XREAL_1:21; :: thesis: verum

end;

assume A21: for f being RealMap of T st f is continuous holds
f is with_max ; :: thesis: for f being RealMap of T st f is continuous holds
f is bounded
let f be RealMap of T; :: thesis: ( f is continuous implies f is bounded )
assume A22: f is continuous ; :: thesis: f is bounded
then f is with_max by A21;
then f .: the carrier of T is right_end by MEASURE6:def 16;
then f .: the carrier of T is bounded_above ;
hence f is bounded_above by MEASURE6:def 15; :: according to SEQ_2:def 8 :: thesis: f is bounded_below
f is with_min by A21, A22, Th60;
then f .: the carrier of T is left_end by MEASURE6:def 17;
then f .: the carrier of T is bounded_below ;
hence f is bounded_below by MEASURE6:def 14; :: thesis: verum