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;

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

( - 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

then A4:
rng (- f) c= REAL
;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;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

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