let X be non empty set ; :: thesis: for f being PartFunc of X,REAL holds
( max+ (R_EAL f) = R_EAL (max+ f) & max- (R_EAL f) = R_EAL (max- f) )
let f be PartFunc of X,REAL; :: thesis: ( max+ (R_EAL f) = R_EAL (max+ f) & max- (R_EAL f) = R_EAL (max- f) )
dom (max+ (R_EAL f)) = dom (R_EAL f) by MESFUNC2:def 2;
then dom (max+ (R_EAL f)) = dom f by MESFUNC5:def 7;
then A1: dom (max+ (R_EAL f)) = dom (max+ f) by RFUNCT_3:def 10;
then A2: dom (max+ (R_EAL f)) = dom (R_EAL (max+ f)) by MESFUNC5:def 7;
dom (max- (R_EAL f)) = dom (R_EAL f) by MESFUNC2:def 3;
then dom (max- (R_EAL f)) = dom f by MESFUNC5:def 7;
then A3: dom (max- (R_EAL f)) = dom (max- f) by RFUNCT_3:def 11;
then A4: dom (max- (R_EAL f)) = dom (R_EAL (max- f)) by MESFUNC5:def 7;
for x being Element of X st x in dom (max+ (R_EAL f)) holds
(max+ (R_EAL f)) . x = (R_EAL (max+ f)) . x

proof

let x be Element of X; :: thesis: ( x in dom (max+ (R_EAL f)) implies (max+ (R_EAL f)) . x = (R_EAL (max+ f)) . x )
assume A5: x in dom (max+ (R_EAL f)) ; :: thesis: (max+ (R_EAL f)) . x = (R_EAL (max+ f)) . x

per cases ( f . x >= 0 or f . x < 0 ) ;

suppose A6: f . x >= 0 ; :: thesis: (max+ (R_EAL f)) . x = (R_EAL (max+ f)) . x

then A7: (R_EAL f) . x >= 0 by MESFUNC5:def 7;
(max+ (R_EAL f)) . x = max (((R_EAL f) . x),0) by A5, MESFUNC2:def 2;
then (max+ (R_EAL f)) . x = (R_EAL f) . x by A7, XXREAL_0:def 10;
then (max+ (R_EAL f)) . x = f . x by MESFUNC5:def 7;
then (max+ (R_EAL f)) . x = max ((f . x),0) by A6, XXREAL_0:def 10;
then (max+ (R_EAL f)) . x = max+ (f . x) by RFUNCT_3:def 1;
then (max+ (R_EAL f)) . x = (max+ f) . x by A1, A5, RFUNCT_3:def 10;
hence (max+ (R_EAL f)) . x = (R_EAL (max+ f)) . x by MESFUNC5:def 7; :: thesis: verum

end;

suppose A8: f . x < 0 ; :: thesis: (max+ (R_EAL f)) . x = (R_EAL (max+ f)) . x

then A9: (R_EAL f) . x < 0 by MESFUNC5:def 7;
(max+ (R_EAL f)) . x = max (((R_EAL f) . x),0) by A5, MESFUNC2:def 2;
then (max+ (R_EAL f)) . x = 0 by A9, XXREAL_0:def 10;
then (max+ (R_EAL f)) . x = max ((f . x),0) by A8, XXREAL_0:def 10;
then (max+ (R_EAL f)) . x = max+ (f . x) by RFUNCT_3:def 1;
then (max+ (R_EAL f)) . x = (max+ f) . x by A1, A5, RFUNCT_3:def 10;
hence (max+ (R_EAL f)) . x = (R_EAL (max+ f)) . x by MESFUNC5:def 7; :: thesis: verum

end;

end;

end;

hence max+ (R_EAL f) = R_EAL (max+ f) by A2, PARTFUN1:5; :: thesis: max- (R_EAL f) = R_EAL (max- f)
for x being Element of X st x in dom (max- (R_EAL f)) holds
(max- (R_EAL f)) . x = (R_EAL (max- f)) . x

proof

let x be Element of X; :: thesis: ( x in dom (max- (R_EAL f)) implies (max- (R_EAL f)) . x = (R_EAL (max- f)) . x )
assume A10: x in dom (max- (R_EAL f)) ; :: thesis: (max- (R_EAL f)) . x = (R_EAL (max- f)) . x

per cases ( f . x <= 0 or f . x > 0 ) ;

suppose A11: f . x <= 0 ; :: thesis: (max- (R_EAL f)) . x = (R_EAL (max- f)) . x

then A12: (R_EAL f) . x <= 0 by MESFUNC5:def 7;
(max- (R_EAL f)) . x = max ((- ((R_EAL f) . x)),0) by A10, MESFUNC2:def 3;
then (max- (R_EAL f)) . x = - ((R_EAL f) . x) by A12, XXREAL_0:def 10;
then (max- (R_EAL f)) . x = - (f . x) by MESFUNC5:def 7;
then (max- (R_EAL f)) . x = max ((- (f . x)),0) by A11, XXREAL_0:def 10;
then (max- (R_EAL f)) . x = max- (f . x) by RFUNCT_3:def 2;
then (max- (R_EAL f)) . x = (max- f) . x by A3, A10, RFUNCT_3:def 11;
hence (max- (R_EAL f)) . x = (R_EAL (max- f)) . x by MESFUNC5:def 7; :: thesis: verum

end;

suppose A13: f . x > 0 ; :: thesis: (max- (R_EAL f)) . x = (R_EAL (max- f)) . x

then A14: (R_EAL f) . x > 0 by MESFUNC5:def 7;
(max- (R_EAL f)) . x = max ((- ((R_EAL f) . x)),0) by A10, MESFUNC2:def 3;
then (max- (R_EAL f)) . x = 0 by A14, XXREAL_0:def 10;
then (max- (R_EAL f)) . x = max ((- (f . x)),0) by A13, XXREAL_0:def 10;
then (max- (R_EAL f)) . x = max- (f . x) by RFUNCT_3:def 2;
then (max- (R_EAL f)) . x = (max- f) . x by A3, A10, RFUNCT_3:def 11;
hence (max- (R_EAL f)) . x = (R_EAL (max- f)) . x by MESFUNC5:def 7; :: thesis: verum

end;

end;

end;

hence max- (R_EAL f) = R_EAL (max- f) by A4, PARTFUN1:5; :: thesis: verum