let X be non empty set ; :: thesis: for f, g being PartFunc of X, ExtREAL st f is without-infty & f is without+infty & g is without-infty & g is without+infty 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 without-infty & f is without+infty & g is without-infty & g is without+infty implies ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g) )
assume A1: ( f is without-infty & f is without+infty & g is without-infty & g is without+infty ) ; :: thesis: ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
then dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) by Th30;
then A2: dom (((max+ (f + g)) + (max- f)) + (max- g)) = dom (((max- (f + g)) + (max+ f)) + (max+ g)) by A1, Th30;
A3: ( dom (max+ (f + g)) = dom (f + g) & dom (max- (f + g)) = dom (f + g) & dom (max+ f) = dom f & dom (max- f) = dom f & dom (max+ g) = dom g & dom (max- g) = dom g ) by MESFUNC2:def 2, MESFUNC2:def 3;
( ( for x being set st x in dom (max+ (f + g)) holds
0 <= (max+ (f + g)) . x ) & ( for x being set st x in dom (max- (f + g)) holds
0 <= (max- (f + g)) . x ) & ( for x being set st x in dom (max+ f) holds
0 <= (max+ f) . x ) & ( for x being set st x in dom (max- f) holds
0 <= (max- f) . x ) & ( for x being set st x in dom (max+ g) holds
0 <= (max+ g) . x ) & ( for x being set st x in dom (max- g) holds
0 <= (max- g) . x ) ) by MESFUNC2:14, MESFUNC2:15;
then A4: ( max+ (f + g) is nonnegative & max- (f + g) is nonnegative & max+ f is nonnegative & max- f is nonnegative & max+ g is nonnegative & max- g is nonnegative ) by SUPINF_2:71;
then A5: dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom (f + g)) /\ (dom f)) /\ (dom g) by A3, Th29;
then A6: dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom (f + g)) /\ ((dom f) /\ (dom g)) by XBOOLE_1:16;
for x being set 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 set ; :: 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 A7: 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 A8: (((max- (f + g)) + (max+ f)) + (max+ g)) . x = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A3, A4, A5, Th29;
A9: dom (f + g) = (dom f) /\ (dom g) by A1, Th22;
then A10: (max+ (f + g)) . x = max ((f + g) . x),0 by A3, A6, A7, MESFUNC2:def 2
.= max ((f . x) + (g . x)),0 by A6, A7, A9, MESFUNC1:def 3 ;
A11: (max- (f + g)) . x = max (- ((f + g) . x)),0 by A3, A6, A7, A9, MESFUNC2:def 3
.= max (- ((f . x) + (g . x))),0 by A6, A7, A9, MESFUNC1:def 3 ;
A12: ( x in dom f & x in dom g ) by A6, A7, A9, XBOOLE_0:def 4;
then A13: ( (max+ f) . x = max (f . x),0 & (max- f) . x = max (- (f . x)),0 & (max+ g) . x = max (g . x),0 & (max- g) . x = max (- (g . x)),0 ) by A3, MESFUNC2:def 2, MESFUNC2:def 3;
A14: ( f . x <> +infty & f . x <> -infty & g . x <> +infty & g . x <> -infty ) by A1, A12, Th16, Th17;
then A15: ( - (f . x) <> +infty & - (f . x) <> -infty & - (g . x) <> +infty & - (g . x) <> -infty ) by EXTREAL1:4;
A16: dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom (max+ (f + g))) /\ (dom (max- f))) /\ (dom (max- g)) by A4, Th29;

now

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

suppose A17: 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 - (f . x) <= 0 by EXTREAL1:25;
then A18: (max- f) . x = 0 by A13, XXREAL_0:def 10;

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

suppose A19: 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 A20: 0 <= (f . x) + (g . x) by A17, EXTREAL2:7;
then ( - (g . x) <= 0 & - ((f . x) + (g . x)) <= 0 ) by A19, EXTREAL1:25;
then A21: ( (max- g) . x = 0 & (max- (f + g)) . x = 0 ) by A11, A13, XXREAL_0:def 10;
then A22: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + (R_EAL 0 )) + (R_EAL 0 ) by A10, A18, A20, XXREAL_0:def 10
.= ((f . x) + (g . x)) + (R_EAL 0 ) by SUPINF_2:18
.= (f . x) + (g . x) by SUPINF_2:18 ;
(max+ g) . x = g . x by A13, A19, XXREAL_0:def 10;
then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((R_EAL 0 ) + (f . x)) + (g . x) by A13, A17, A21, 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 A22, SUPINF_2:18; :: thesis: verum

end;

suppose A23: 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 0 <= - (g . x) by EXTREAL1:25;
then A24: ( (max- g) . x = - (g . x) & (max+ g) . x = 0 ) by A13, A23, XXREAL_0:def 10;

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

suppose A25: 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 - ((f . x) + (g . x)) <= 0 by EXTREAL1:25;
then (max- (f + g)) . x = 0 by A11, XXREAL_0:def 10;
then A26: (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((R_EAL 0 ) + (f . x)) + (R_EAL 0 ) by A13, A17, A24, XXREAL_0:def 10;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + (R_EAL 0 )) + (- (g . x)) by A10, A18, A24, A25, XXREAL_0:def 10
.= ((f . x) + (g . x)) - (g . x) by SUPINF_2:18
.= (f . x) + ((g . x) - (g . x)) by A14, EXTREAL1:11
.= (f . x) + (R_EAL 0 ) by EXTREAL1:9 ;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A26, SUPINF_2:18; :: thesis: verum

end;

suppose A27: (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 0 <= - ((f . x) + (g . x)) by EXTREAL1:25;
then A28: (max- (f + g)) . x = - ((f . x) + (g . x)) by A11, XXREAL_0:def 10;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = ((R_EAL 0 ) + (R_EAL 0 )) + (- (g . x)) by A10, A18, A24, A27, XXREAL_0:def 10;
then A29: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (R_EAL 0 ) + (- (g . x)) by SUPINF_2:18;
(((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + (f . x)) + (R_EAL 0 ) by A13, A17, A24, A28, XXREAL_0:def 10
.= (- ((f . x) + (g . x))) + (f . x) by SUPINF_2:18
.= ((- (g . x)) - (f . x)) + (f . x) by EXTREAL2:14
.= (- (g . x)) + ((- (f . x)) + (f . x)) by A15, EXTREAL1:8 ;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A29, EXTREAL1:9; :: thesis: verum

end;

end;

end;

end;

end;

suppose A30: 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 0 <= - (f . x) by EXTREAL1:25;
then A31: (max- f) . x = - (f . x) by A13, XXREAL_0:def 10;

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

suppose A32: 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 - (g . x) <= 0 by EXTREAL1:25;
then A33: (max- g) . x = 0 by A13, XXREAL_0:def 10;
A34: (max+ g) . x = g . x by A13, A32, XXREAL_0:def 10;

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

suppose A35: 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 - ((f . x) + (g . x)) <= 0 by EXTREAL1:25;
then A36: (max- (f + g)) . x = 0 by A11, XXREAL_0:def 10;
A37: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + (- (f . x))) + (R_EAL 0 ) by A10, A31, A33, A35, XXREAL_0:def 10
.= ((f . x) + (g . x)) + (- (f . x)) by SUPINF_2:18
.= (g . x) + ((f . x) + (- (f . x))) by A14, EXTREAL1:8
.= (g . x) + (R_EAL 0 ) by EXTREAL1:9 ;
(((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((R_EAL 0 ) + (R_EAL 0 )) + (g . x) by A13, A30, A34, A36, 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 A37, SUPINF_2:18; :: thesis: verum

end;

suppose A38: (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 0 <= - ((f . x) + (g . x)) by EXTREAL1:25;
then A39: (max- (f + g)) . x = - ((f . x) + (g . x)) by A11, XXREAL_0:def 10;
A40: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = ((R_EAL 0 ) + (- (f . x))) + (R_EAL 0 ) by A10, A31, A33, A38, XXREAL_0:def 10
.= (R_EAL 0 ) + (- (f . x)) by SUPINF_2:18 ;
(((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + (R_EAL 0 )) + (g . x) by A13, A30, A34, A39, XXREAL_0:def 10
.= (- ((f . x) + (g . x))) + (g . x) by SUPINF_2:18
.= ((- (f . x)) - (g . x)) + (g . x) by EXTREAL2:14
.= (- (f . x)) + ((- (g . x)) + (g . x)) by A15, EXTREAL1:8 ;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A40, EXTREAL1:9; :: thesis: verum

end;

end;

end;

suppose A41: 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 A42: (f . x) + (g . x) <= 0 by A30, EXTREAL2:9;
0 <= - (g . x) by A41, EXTREAL1:25;
then A43: (max- g) . x = - (g . x) by A13, XXREAL_0:def 10;
0 <= - ((f . x) + (g . x)) by A42, EXTREAL1:25;
then A44: (max- (f + g)) . x = - ((f . x) + (g . x)) by A11, XXREAL_0:def 10;
A45: (max+ g) . x = 0 by A13, A41, XXREAL_0:def 10;
A46: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = ((R_EAL 0 ) + (- (f . x))) + (- (g . x)) by A10, A31, A42, A43, XXREAL_0:def 10
.= (- (f . x)) - (g . x) by SUPINF_2:18 ;
(((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + (R_EAL 0 )) + (R_EAL 0 ) by A13, A30, A44, A45, XXREAL_0:def 10
.= (- ((f . x) + (g . x))) + (R_EAL 0 ) by SUPINF_2:18
.= - ((f . x) + (g . x)) by SUPINF_2:18 ;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A46, EXTREAL2:14; :: thesis: verum

end;

end;

end;

end;

end;

hence (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x by A4, A7, A8, A16, Th29; :: thesis: verum

end;

hence ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g) by A2, FUNCT_1:9; :: thesis: verum