let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL holds
( rng (max+ f) c= (rng f) \/ & rng (max- f) c= (rng (- f)) \/ )

let f be PartFunc of X,ExtREAL; :: thesis: ( rng (max+ f) c= (rng f) \/ & rng (max- f) c= (rng (- f)) \/ )
now :: thesis: for y being object st y in rng (max+ f) holds
y in (rng f) \/
let y be object ; :: thesis: ( y in rng (max+ f) implies b1 in (rng f) \/ )
assume y in rng (max+ f) ; :: thesis: b1 in (rng f) \/
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 ;
A3: y = max ((f . x),0) by ;
per cases ( y = f . x or y = 0 ) by ;
end;
end;
hence rng (max+ f) c= (rng f) \/ ; :: thesis: rng (max- f) c= (rng (- f)) \/
now :: thesis: for y being object st y in rng (max- f) holds
y in (rng (- f)) \/
let y be object ; :: thesis: ( y in rng (max- f) implies b1 in (rng (- f)) \/ )
assume y in rng (max- f) ; :: thesis: b1 in (rng (- f)) \/
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 ;
then A5: x in dom (- f) by MESFUNC1:def 7;
y = max ((- (f . x)),0) by ;
per cases then ( y = - (f . x) or y = 0 ) by XXREAL_0:16;
suppose y = - (f . x) ; :: thesis: b1 in (rng (- f)) \/
then y = (- f) . x by ;
then y in rng (- f) by ;
hence y in (rng (- f)) \/ by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence rng (max- f) c= (rng (- f)) \/ ; :: thesis: verum