let X be non empty set ; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let r be Real; :: thesis:

hereby :: thesis:

assume A1: r > 0 ; :: thesis:
reconsider r1 = r as ExtReal ;

let x be Element of X; :: thesis:
assume x in less_dom ((max+ f),r) ; :: thesis:
then A2: ( x in dom (max+ f) & (max+ f) . x < r ) by MESFUNC1:def 11;
then A3: x in dom f by MESFUNC2:def 2;
max ((f . x),0) < r1 by A2, MESFUNC2:def 2;
then f . x < r1 by XXREAL_0:31;
hence x in less_dom (f,r) by A3, MESFUNC1:def 11; :: thesis:

end;

then A4: less_dom ((max+ f),r) c= less_dom (f,r) ;

let x be Element of X; :: thesis:
assume x in less_dom (f,r) ; :: thesis:
then A5: ( x in dom f & f . x < r ) by MESFUNC1:def 11;
then A6: x in dom (max+ f) by MESFUNC2:def 2;
then (max+ f) . x = max ((f . x),0) by MESFUNC2:def 2;
then (max+ f) . x < r by A1, A5, XXREAL_0:29;
hence x in less_dom ((max+ f),r) by A6, MESFUNC1:def 11; :: thesis:

end;

then less_dom (f,r) c= less_dom ((max+ f),r) ;
hence less_dom ((max+ f),r) = less_dom (f,r) by A4; :: thesis:

end;

assume A7: r <= 0 ; :: thesis:
reconsider r1 = r as ExtReal ;

let x be Element of X; :: thesis:
assume x in great_dom ((max- f),(- r)) ; :: thesis:
then A8: ( x in dom (max- f) & (max- f) . x > - r ) by MESFUNC1:def 13;
then A9: x in dom f by MESFUNC2:def 3;
A10: max ((- (f . x)),0) > - r1 by A8, MESFUNC2:def 3;

assume 0 > - (f . x) ; :: thesis:
then max ((- (f . x)),0) = 0 by XXREAL_0:def 10;
hence contradiction by A7, A10; :: thesis:

end;

then max ((- (f . x)),0) = - (f . x) by XXREAL_0:def 10;
then f . x < r1 by A10, XXREAL_3:38;
hence x in less_dom (f,r) by A9, MESFUNC1:def 11; :: thesis:

end;

then A11: great_dom ((max- f),(- r)) c= less_dom (f,r) ;

let x be Element of X; :: thesis:
assume x in less_dom (f,r) ; :: thesis:
then A12: ( x in dom f & f . x < r ) by MESFUNC1:def 11;
then A13: x in dom (max- f) by MESFUNC2:def 3;
max ((- (f . x)),0) = - (f . x) by A7, A12, XXREAL_0:def 10;
then (max- f) . x = - (f . x) by A13, MESFUNC2:def 3;
then (max- f) . x > - r1 by A12, XXREAL_3:38;
hence x in great_dom ((max- f),(- r)) by A13, MESFUNC1:def 13; :: thesis:

end;

then less_dom (f,r) c= great_dom ((max- f),(- r)) ;
hence great_dom ((max- f),(- r)) = less_dom (f,r) by A11; :: thesis: