let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL st f is V55() holds
( - f is V55() & max+ f is V55() & max- f is V55() )
let f be PartFunc of X,ExtREAL; :: thesis: ( f is V55() implies ( - f is V55() & max+ f is V55() & max- f is V55() ) )
assume f is V55() ; :: thesis: ( - f is V55() & max+ f is V55() & max- f is V55() )
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 V55() by VALUED_0:def 3; :: thesis: ( max+ f is V55() & max- f is V55() )
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 V55() by VALUED_0:def 3; :: thesis: max- f is V55()
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 V55() by VALUED_0:def 3; :: thesis: verum