let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL
for x being Element of X holds
( (max+ f) . x <= |.f.| . x & (max- f) . x <= |.f.| . x )
let f be PartFunc of X,ExtREAL; :: thesis: for x being Element of X holds
( (max+ f) . x <= |.f.| . x & (max- f) . x <= |.f.| . x )
let x be Element of X; :: thesis: ( (max+ f) . x <= |.f.| . x & (max- f) . x <= |.f.| . x )
A1: - (f . x) <= - (- |.(f . x).|) by XXREAL_3:38, EXTREAL1:20;
( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) ) by MESFUNC2:18;
then A2: ( (max+ f) . x <= |.(f . x).| & (max- f) . x <= |.(f . x).| ) by A1, EXTREAL1:14, EXTREAL1:20;

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

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

hence ( (max+ f) . x <= |.f.| . x & (max- f) . x <= |.f.| . x ) by A2, MESFUNC1:def 10; :: thesis: verum

end;

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

then not x in dom f by MESFUNC1:def 10;
then ( f . x = 0 & |.f.| . x = 0 ) by A3, FUNCT_1:def 2;
hence ( (max+ f) . x <= |.f.| . x & (max- f) . x <= |.f.| . x ) by A1, MESFUNC2:18; :: thesis: verum

end;

end;