let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL
for x being object holds
( f . x <= (max+ f) . x & f . x >= - ((max- f) . x) )
let f be PartFunc of X,ExtREAL; :: thesis: for x being object holds
( f . x <= (max+ f) . x & f . x >= - ((max- f) . x) )
let x be object ; :: thesis: ( f . x <= (max+ f) . x & f . x >= - ((max- f) . x) )

per cases ( x in dom f or not x in dom f ) ;

suppose x in dom f ; :: thesis: ( f . x <= (max+ f) . x & f . x >= - ((max- f) . x) )

then ( x in dom (max+ f) & x in dom (max- f) ) by MESFUNC2:def 2, MESFUNC2:def 3;
then A1: ( (max+ f) . x = max ((f . x),0) & (max- f) . x = max ((- (f . x)),0) ) by MESFUNC2:def 2, MESFUNC2:def 3;
reconsider a = (max- f) . x, b = - (f . x) as ExtReal ;
- b >= - a by A1, XXREAL_0:25, XXREAL_3:38;
hence ( f . x <= (max+ f) . x & f . x >= - ((max- f) . x) ) by A1, XXREAL_0:25; :: thesis: verum

end;

suppose A2: not x in dom f ; :: thesis: ( f . x <= (max+ f) . x & f . x >= - ((max- f) . x) )

then ( not x in dom (max+ f) & not x in dom (max- f) ) by MESFUNC2:def 2, MESFUNC2:def 3;
then ( f . x = 0 & (max+ f) . x = 0 & (max- f) . x = 0 ) by A2, FUNCT_1:def 2;
hence ( f . x <= (max+ f) . x & f . x >= - ((max- f) . x) ) ; :: thesis: verum

end;

end;