let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st f is () & f is () & g is () & g is () holds
((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is () & f is () & g is () & g is () implies ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g) )
assume that
A1: f is () and
A2: f is () and
A3: g is () and
A4: g is () ; :: thesis: ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
A5: dom (max- (f + g)) = dom (f + g) by MESFUNC2:def 3;
for x being object st x in dom (max- g) holds
0 <= (max- g) . x by MESFUNC2:13;
then A6: max- g is nonnegative by SUPINF_2:52;
for x being object st x in dom (max+ g) holds
0 <= (max+ g) . x by MESFUNC2:12;
then A7: max+ g is nonnegative by SUPINF_2:52;
A8: dom (max- f) = dom f by MESFUNC2:def 3;
for x being object st x in dom (max+ (f + g)) holds
0 <= (max+ (f + g)) . x by MESFUNC2:12;
then A9: max+ (f + g) is nonnegative by SUPINF_2:52;
for x being object st x in dom (max+ f) holds
0 <= (max+ f) . x by MESFUNC2:12;
then A10: max+ f is nonnegative by SUPINF_2:52;
A11: dom (max+ f) = dom f by MESFUNC2:def 2;
A12: dom (max+ g) = dom g by MESFUNC2:def 2;
A13: dom (max- g) = dom g by MESFUNC2:def 3;
for x being object st x in dom (max- f) holds
0 <= (max- f) . x by MESFUNC2:13;
then A14: max- f is nonnegative by SUPINF_2:52;
A15: dom (max+ (f + g)) = dom (f + g) by MESFUNC2:def 2;
then A16: dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom (f + g)) /\ (dom f)) /\ (dom g) by A8, A13, A9, A14, A6, Th23;
then A17: dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom (f + g)) /\ ((dom f) /\ (dom g)) by XBOOLE_1:16;
for x being object st x in dom (max- (f + g)) holds
0 <= (max- (f + g)) . x by MESFUNC2:13;
then A18: max- (f + g) is nonnegative by SUPINF_2:52;
A19: for x being object st x in dom (((max+ (f + g)) + (max- f)) + (max- g)) holds
(((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x

proof

let x be object ; :: thesis: ( x in dom (((max+ (f + g)) + (max- f)) + (max- g)) implies (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x )
assume A20: x in dom (((max+ (f + g)) + (max- f)) + (max- g)) ; :: thesis: (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x
then A21: x in dom g by A16, XBOOLE_0:def 4;
then A22: (max+ g) . x = max ((g . x),0) by A12, MESFUNC2:def 2;
A23: g . x <> +infty by A4;
A24: dom (f + g) = (dom f) /\ (dom g) by A1, A3, Th16;
then A25: (max+ (f + g)) . x = max (((f + g) . x),0) by A15, A17, A20, MESFUNC2:def 2
.= max (((f . x) + (g . x)),0) by A17, A20, A24, MESFUNC1:def 3 ;
A26: x in dom f by A17, A20, A24, XBOOLE_0:def 4;
then A27: (max+ f) . x = max ((f . x),0) by A11, MESFUNC2:def 2;
A28: (max- (f + g)) . x = max ((- ((f + g) . x)),0) by A5, A17, A20, A24, MESFUNC2:def 3
.= max ((- ((f . x) + (g . x))),0) by A17, A20, A24, MESFUNC1:def 3 ;
A29: f . x <> -infty by A1;
then A30: - (f . x) <> +infty by XXREAL_3:23;
A31: f . x <> +infty by A2;
A32: (max- f) . x = max ((- (f . x)),0) by A8, A26, MESFUNC2:def 3;
A33: (max- g) . x = max ((- (g . x)),0) by A13, A21, MESFUNC2:def 3;
A34: g . x <> -infty by A3;
then A35: - (g . x) <> +infty by XXREAL_3:23;

A36: now :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)

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

suppose A37: 0 <= f . x ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)

then A38: (max- f) . x = 0 by A32, XXREAL_0:def 10;

per cases ( 0 <= g . x or g . x < 0 ) ;

suppose A39: 0 <= g . x ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)

then (max- g) . x = 0 by A33, XXREAL_0:def 10;
then A40: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + 0) + 0 by A25, A37, A38, A39, XXREAL_0:def 10
.= ((f . x) + (g . x)) + 0 by XXREAL_3:4
.= (f . x) + (g . x) by XXREAL_3:4 ;
A41: (max+ g) . x = g . x by A22, A39, XXREAL_0:def 10;
(max- (f + g)) . x = 0 by A28, A37, A39, XXREAL_0:def 10;
then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = (0 + (f . x)) + (g . x) by A27, A37, A41, XXREAL_0:def 10;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A40, XXREAL_3:4; :: thesis: verum

end;

suppose A42: g . x < 0 ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)

then A43: (max+ g) . x = 0 by A22, XXREAL_0:def 10;
A44: (max- g) . x = - (g . x) by A33, A42, XXREAL_0:def 10;

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

suppose A45: 0 <= (f . x) + (g . x) ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)

then (max- (f + g)) . x = 0 by A28, XXREAL_0:def 10;
then A46: (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = (0 + (f . x)) + 0 by A27, A37, A43, XXREAL_0:def 10;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + 0) + (- (g . x)) by A25, A38, A44, A45, XXREAL_0:def 10
.= ((f . x) + (g . x)) - (g . x) by XXREAL_3:4
.= (f . x) + ((g . x) - (g . x)) by A23, A34, XXREAL_3:30
.= (f . x) + 0 by XXREAL_3:7 ;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A46, XXREAL_3:4; :: thesis: verum

end;

suppose A47: (f . x) + (g . x) < 0 ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)

then (max+ (f + g)) . x = 0 by A25, XXREAL_0:def 10;
then (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (0 + 0) + (- (g . x)) by A38, A44;
then A48: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = 0 + (- (g . x)) ;
(max- (f + g)) . x = - ((f . x) + (g . x)) by A28, A47, XXREAL_0:def 10;
then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + (f . x)) + 0 by A27, A37, A43, XXREAL_0:def 10
.= (- ((f . x) + (g . x))) + (f . x) by XXREAL_3:4
.= ((- (g . x)) - (f . x)) + (f . x) by XXREAL_3:25
.= (- (g . x)) + ((- (f . x)) + (f . x)) by A31, A30, A35, XXREAL_3:29 ;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A48, XXREAL_3:7; :: thesis: verum

end;

end;

end;

end;

end;

suppose A49: f . x < 0 ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)

then A50: (max- f) . x = - (f . x) by A32, XXREAL_0:def 10;

per cases ( 0 <= g . x or g . x < 0 ) ;

suppose A51: 0 <= g . x ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)

then A52: (max+ g) . x = g . x by A22, XXREAL_0:def 10;
A53: (max- g) . x = 0 by A33, A51, XXREAL_0:def 10;

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

suppose A54: 0 <= (f . x) + (g . x) ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)

then A55: (max- (f + g)) . x = 0 by A28, XXREAL_0:def 10;
(max+ f) . x = 0 by A27, A49, XXREAL_0:def 10;
then A56: (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = (0 + 0) + (g . x) by A52, A55;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + (- (f . x))) + 0 by A25, A50, A53, A54, XXREAL_0:def 10
.= ((f . x) + (g . x)) + (- (f . x)) by XXREAL_3:4
.= (g . x) + ((f . x) - (f . x)) by A31, A29, A23, A34, XXREAL_3:29
.= (g . x) + 0 by XXREAL_3:7 ;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A56; :: thesis: verum

end;

suppose A57: (f . x) + (g . x) < 0 ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)

then (max- (f + g)) . x = - ((f . x) + (g . x)) by A28, XXREAL_0:def 10;
then A58: (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + 0) + (g . x) by A27, A49, A52, XXREAL_0:def 10
.= (- ((f . x) + (g . x))) + (g . x) by XXREAL_3:4
.= ((- (f . x)) - (g . x)) + (g . x) by XXREAL_3:25
.= (- (f . x)) + ((- (g . x)) + (g . x)) by A23, A30, A35, XXREAL_3:29 ;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (0 + (- (f . x))) + 0 by A25, A50, A53, A57, XXREAL_0:def 10
.= 0 + (- (f . x)) by XXREAL_3:4 ;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A58, XXREAL_3:7; :: thesis: verum

end;

end;

end;

suppose A59: g . x < 0 ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)

then (max- g) . x = - (g . x) by A33, XXREAL_0:def 10;
then A60: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (0 + (- (f . x))) + (- (g . x)) by A25, A49, A50, A59, XXREAL_0:def 10
.= (- (f . x)) - (g . x) by XXREAL_3:4 ;
A61: (max+ g) . x = 0 by A22, A59, XXREAL_0:def 10;
(max- (f + g)) . x = - ((f . x) + (g . x)) by A28, A49, A59, XXREAL_0:def 10;
then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + 0) + 0 by A27, A49, A61, XXREAL_0:def 10
.= (- ((f . x) + (g . x))) + 0 by XXREAL_3:4
.= - ((f . x) + (g . x)) by XXREAL_3:4 ;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A60, XXREAL_3:25; :: thesis: verum

end;

end;

end;

end;

end;

A62: dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom (max+ (f + g))) /\ (dom (max- f))) /\ (dom (max- g)) by A9, A14, A6, Th23;
(((max- (f + g)) + (max+ f)) + (max+ g)) . x = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A5, A11, A12, A18, A10, A7, A16, A20, Th23;
hence (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x by A9, A14, A6, A20, A62, A36, Th23; :: thesis: verum

end;

dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) by A1, A3, Th24;
then dom (((max+ (f + g)) + (max- f)) + (max- g)) = dom (((max- (f + g)) + (max+ f)) + (max+ g)) by A1, A3, Th24;
hence ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g) by A19, FUNCT_1:2; :: thesis: verum