let C be non empty set ; :: thesis: for X being set
for f being PartFunc of C,REAL st f | X is bounded_below holds
(max- f) | X is bounded_above
let X be set ; :: thesis: for f being PartFunc of C,REAL st f | X is bounded_below holds
(max- f) | X is bounded_above
let f be PartFunc of C,REAL ; :: thesis: ( f | X is bounded_below implies (max- f) | X is bounded_above )
assume f | X is bounded_below ; :: thesis: (max- f) | X is bounded_above
then consider b being real number such that
A1: for c being set st c in X /\ (dom f) holds
f . c >= b by RFUNCT_1:88;
A2: dom (max- f) = dom f by RFUNCT_3:def 11;
ex r being Real st
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r

proof

now

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

suppose A3: b > 0 ; :: thesis: ex r being Real st
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r

for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= 0

proof

let c be set ; :: thesis: ( c in X /\ (dom (max- f)) implies (max- f) . c <= 0 )
assume c in X /\ (dom (max- f)) ; :: thesis: (max- f) . c <= 0
then A4: c in X /\ (dom f) by RFUNCT_3:def 11;
then f . c >= b by A1;
then - (f . c) <= 0 by A3;
then max (- (f . c)),0 = 0 by XXREAL_0:def 10;
then A5: max- (f . c) = 0 by RFUNCT_3:def 2;
c in dom f by A4, XBOOLE_0:def 4;
hence (max- f) . c <= 0 by A2, A5, RFUNCT_3:def 11; :: thesis: verum

end;

then consider r being Real such that
A6: ( r = 0 & ( for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r ) ) ;
thus ex r being Real st
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r by A6; :: thesis: verum

end;

suppose b <= 0 ; :: thesis: ex r being Real st
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r

then A7: - b >= - 0 ;
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= - b

proof

let c be set ; :: thesis: ( c in X /\ (dom (max- f)) implies (max- f) . c <= - b )
assume c in X /\ (dom (max- f)) ; :: thesis: (max- f) . c <= - b
then A8: c in X /\ (dom f) by RFUNCT_3:def 11;
then f . c >= b by A1;
then - (f . c) <= - b by XREAL_1:26;
then max (- (f . c)),0 <= - b by A7, XXREAL_0:28;
then A9: max- (f . c) <= - b by RFUNCT_3:def 2;
c in dom f by A8, XBOOLE_0:def 4;
hence (max- f) . c <= - b by A2, A9, RFUNCT_3:def 11; :: thesis: verum

end;

then consider r being real number such that
A10: ( r = - b & ( for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r ) ) ;
r is Real by XREAL_0:def 1;
hence ex r being Real st
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r by A10; :: thesis: verum

end;

end;

end;

then consider r being Real such that
A11: for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r ;
thus ex r being Real st
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r by A11; :: thesis: verum

end;

hence (max- f) | X is bounded_above by RFUNCT_1:87; :: thesis: verum