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} )

now :: thesis: for y being object st y in rng (max+ f) holds
y in (rng f) \/ {0}

let y be object ; :: thesis: ( y in rng (max+ f) implies b₁ in (rng f) \/ {0} )
assume y in rng (max+ f) ; :: thesis: b₁ 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;

per cases ( y = f . x or y = 0 ) by A3, XXREAL_0:16;

suppose y = f . x ; :: thesis: b₁ in (rng f) \/ {0}

then y in rng f by A2, FUNCT_1:3;
hence y in (rng f) \/ {0} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose y = 0 ; :: thesis: b₁ in (rng f) \/ {0}

then y in {0} by TARSKI:def 1;
hence y in (rng f) \/ {0} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence rng (max+ f) c= (rng f) \/ {0} ; :: thesis: 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}

let y be object ; :: thesis: ( y in rng (max- f) implies b₁ in (rng (- f)) \/ {0} )
assume y in rng (max- f) ; :: thesis: b₁ 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;

per cases then ( y = - (f . x) or y = 0 ) by XXREAL_0:16;

suppose y = - (f . x) ; :: thesis: b₁ in (rng (- f)) \/ {0}

then y = (- f) . x by A5, MESFUNC1:def 7;
then y in rng (- f) by A5, FUNCT_1:3;
hence y in (rng (- f)) \/ {0} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose y = 0 ; :: thesis: b₁ in (rng (- f)) \/ {0}

then y in {0} by TARSKI:def 1;
hence y in (rng (- f)) \/ {0} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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