let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL st f is real-valued holds
( - f is real-valued & max+ f is real-valued & max- f is real-valued )
let f be PartFunc of X,ExtREAL; :: thesis: ( f is real-valued implies ( - f is real-valued & max+ f is real-valued & max- f is real-valued ) )
assume f is real-valued ; :: thesis: ( - f is real-valued & max+ f is real-valued & max- f is real-valued )
then A1: rng f c= REAL by VALUED_0:def 3;

now :: thesis: for y being object st y in rng (- f) holds
y in REAL

let y be object ; :: thesis: ( y in rng (- f) implies y in REAL )
assume y in rng (- f) ; :: thesis: y in REAL
then consider x being Element of X such that
A2: ( x in dom (- f) & y = (- f) . x ) by PARTFUN1:3;
x in dom f by A2, MESFUNC1:def 7;
then A3: f . x in REAL by A1, FUNCT_1:3;
y = - (f . x) by A2, MESFUNC1:def 7;
hence y in REAL by A3, XREAL_0:def 1; :: thesis: verum

end;

then A4: rng (- f) c= REAL ;
hence - f is real-valued by VALUED_0:def 3; :: thesis: ( max+ f is real-valued & max- f is real-valued )
A5: (rng f) \/ {0} c= REAL by A1, XBOOLE_1:8;
rng (max+ f) c= (rng f) \/ {0} by Th1;
then rng (max+ f) c= REAL by A5;
hence max+ f is real-valued by VALUED_0:def 3; :: thesis: max- f is real-valued
A6: (rng (- f)) \/ {0} c= REAL by A4, XBOOLE_1:8;
rng (max- f) c= (rng (- f)) \/ {0} by Th1;
then rng (max- f) c= REAL by A6;
hence max- f is real-valued by VALUED_0:def 3; :: thesis: verum