let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL
for r being Real holds
( ( r > 0 implies less_dom (f,r) = less_dom ((max+ f),r) ) & ( r <= 0 implies less_dom (f,r) = great_dom ((max- f),(- r)) ) )
let f be PartFunc of X,ExtREAL; :: thesis: for r being Real holds
( ( r > 0 implies less_dom (f,r) = less_dom ((max+ f),r) ) & ( r <= 0 implies less_dom (f,r) = great_dom ((max- f),(- r)) ) )
let r be Real; :: thesis: ( ( r > 0 implies less_dom (f,r) = less_dom ((max+ f),r) ) & ( r <= 0 implies less_dom (f,r) = great_dom ((max- f),(- r)) ) )

hereby :: thesis: ( r <= 0 implies less_dom (f,r) = great_dom ((max- f),(- r)) )

assume A1: r > 0 ; :: thesis: less_dom ((max+ f),r) = less_dom (f,r)
reconsider r1 = r as ExtReal ;

now :: thesis: for x being Element of X st x in less_dom ((max+ f),r) holds
x in less_dom (f,r)

let x be Element of X; :: thesis: ( x in less_dom ((max+ f),r) implies x in less_dom (f,r) )
assume x in less_dom ((max+ f),r) ; :: thesis: x in less_dom (f,r)
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: verum

end;

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

now :: thesis: for x being Element of X st x in less_dom (f,r) holds
x in less_dom ((max+ f),r)

let x be Element of X; :: thesis: ( x in less_dom (f,r) implies x in less_dom ((max+ f),r) )
assume x in less_dom (f,r) ; :: thesis: x in less_dom ((max+ f),r)
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: verum

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: verum

end;

assume A7: r <= 0 ; :: thesis: less_dom (f,r) = great_dom ((max- f),(- r))
reconsider r1 = r as ExtReal ;

now :: thesis: for x being Element of X st x in great_dom ((max- f),(- r)) holds
x in less_dom (f,r)

let x be Element of X; :: thesis: ( x in great_dom ((max- f),(- r)) implies x in less_dom (f,r) )
assume x in great_dom ((max- f),(- r)) ; :: thesis: x in less_dom (f,r)
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;

now :: thesis: not 0 > - (f . x)

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

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: verum

end;

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

now :: thesis: for x being Element of X st x in less_dom (f,r) holds
x in great_dom ((max- f),(- r))

let x be Element of X; :: thesis: ( x in less_dom (f,r) implies x in great_dom ((max- f),(- r)) )
assume x in less_dom (f,r) ; :: thesis: x in great_dom ((max- f),(- r))
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: verum

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: verum