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:
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 ;
then A3: f . x in REAL by ;
y = - (f . x) by ;
hence y in REAL by ; :: 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) \/ c= REAL by ;
rng (max+ f) c= (rng f) \/ 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)) \/ c= REAL by ;
rng (max- f) c= (rng (- f)) \/ by Th1;
then rng (max- f) c= REAL by A6;
hence max- f is V55() by VALUED_0:def 3; :: thesis: verum