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

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

( 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

hence
max+ (R_EAL f) = R_EAL (max+ f)
by A2, PARTFUN1:5; :: thesis: max- (R_EAL f) = R_EAL (max- f)
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

end;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 )
;

end;

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;(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

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;(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

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

hence
max- (R_EAL f) = R_EAL (max- f)
by A4, PARTFUN1:5; :: thesis: verum
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

end;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 )
;

end;

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;(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

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;(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