let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL holds

( rng (max+ f) c= (rng f) \/ {0} & rng (max- f) c= (rng (- f)) \/ {0} )

let f be PartFunc of X,ExtREAL; :: thesis: ( rng (max+ f) c= (rng f) \/ {0} & rng (max- f) c= (rng (- f)) \/ {0} )

( rng (max+ f) c= (rng f) \/ {0} & rng (max- f) c= (rng (- f)) \/ {0} )

let f be PartFunc of X,ExtREAL; :: thesis: ( rng (max+ f) c= (rng f) \/ {0} & rng (max- f) c= (rng (- f)) \/ {0} )

now :: thesis: for y being object st y in rng (max+ f) holds

y in (rng f) \/ {0}

hence
rng (max+ f) c= (rng f) \/ {0}
; :: thesis: rng (max- f) c= (rng (- f)) \/ {0}y in (rng f) \/ {0}

let y be object ; :: thesis: ( y in rng (max+ f) implies b_{1} in (rng f) \/ {0} )

assume y in rng (max+ f) ; :: thesis: b_{1} in (rng f) \/ {0}

then consider x being Element of X such that

A1: ( x in dom (max+ f) & y = (max+ f) . x ) by PARTFUN1:3;

A2: x in dom f by A1, MESFUNC2:def 2;

A3: y = max ((f . x),0) by A1, MESFUNC2:def 2;

end;assume y in rng (max+ f) ; :: thesis: b

then consider x being Element of X such that

A1: ( x in dom (max+ f) & y = (max+ f) . x ) by PARTFUN1:3;

A2: x in dom f by A1, MESFUNC2:def 2;

A3: y = max ((f . x),0) by A1, MESFUNC2:def 2;

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

y in (rng (- f)) \/ {0}

hence
rng (max- f) c= (rng (- f)) \/ {0}
; :: thesis: verumy in (rng (- f)) \/ {0}

let y be object ; :: thesis: ( y in rng (max- f) implies b_{1} in (rng (- f)) \/ {0} )

assume y in rng (max- f) ; :: thesis: b_{1} in (rng (- f)) \/ {0}

then consider x being Element of X such that

A4: ( x in dom (max- f) & y = (max- f) . x ) by PARTFUN1:3;

x in dom f by A4, MESFUNC2:def 3;

then A5: x in dom (- f) by MESFUNC1:def 7;

y = max ((- (f . x)),0) by A4, MESFUNC2:def 3;

end;assume y in rng (max- f) ; :: thesis: b

then consider x being Element of X such that

A4: ( x in dom (max- f) & y = (max- f) . x ) by PARTFUN1:3;

x in dom f by A4, MESFUNC2:def 3;

then A5: x in dom (- f) by MESFUNC1:def 7;

y = max ((- (f . x)),0) by A4, MESFUNC2:def 3;