let X be non empty set ; :: thesis: for f, g being PartFunc of X,REAL holds ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
let f, g be PartFunc of X,REAL ; :: thesis: ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) by Th62;
then A1: dom (((max+ (f + g)) + (max- f)) + (max- g)) = dom (((max- (f + g)) + (max+ f)) + (max+ g)) by Th62;
A2: ( 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 RFUNCT_3:def 10, RFUNCT_3:def 11;
dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom ((max+ (f + g)) + (max- f))) /\ (dom (max- g)) by VALUED_1:def 1
.= ((dom (f + g)) /\ (dom f)) /\ (dom g) by A2, VALUED_1:def 1 ;
then A3: 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 A4: 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 x in (dom f) /\ (dom g) by Th62;
then x in dom (((max- (f + g)) + (max+ f)) + (max+ g)) by Th62;
then A5: (((max- (f + g)) + (max+ f)) + (max+ g)) . x = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by Th60;
A6: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then A7: (max+ (f + g)) . x = max+ ((f + g) . x) by A2, A3, A4, RFUNCT_3:def 10
.= max ((f . x) + (g . x)),0 by A3, A4, A6, VALUED_1:def 1 ;
A8: (max- (f + g)) . x = max- ((f + g) . x) by A2, A3, A4, A6, RFUNCT_3:def 11
.= max (- ((f . x) + (g . x))),0 by A3, A4, A6, VALUED_1:def 1 ;
( x in dom f & x in dom g ) by A3, A4, A6, XBOOLE_0:def 4;
then A9: ( (max+ f) . x = max+ (f . x) & (max- f) . x = max- (f . x) & (max+ g) . x = max+ (g . x) & (max- g) . x = max- (g . x) ) by A2, RFUNCT_3:def 10, RFUNCT_3:def 11;

A10: now

assume A11: 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 ;
then A12: (max- f) . x = 0 by A9, XXREAL_0:def 10;

A13: now

assume A14: 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 A15: 0 + 0 <= (f . x) + (g . x) by A11;
then ( - (g . x) <= 0 & - ((f . x) + (g . x)) <= 0 ) by A14;
then A16: ( (max- g) . x = 0 & (max- (f + g)) . x = 0 ) by A8, A9, XXREAL_0:def 10;
then A17: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (f . x) + (g . x) by A7, A12, A15, XXREAL_0:def 10;
(max+ g) . x = g . x by A9, A14, 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 A9, A11, A16, A17, XXREAL_0:def 10; :: thesis: verum

end;

now

assume A18: g . x < 0 ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
A19: ( (max- g) . x = - (g . x) & (max+ g) . x = 0 ) by A9, A18, XXREAL_0:def 10;

A20: now

assume A21: 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 ;
then A22: (max- (f + g)) . x = 0 by A8, XXREAL_0:def 10;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + 0 ) + (- (g . x)) by A7, A12, A19, 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 A9, A11, A19, A22, XXREAL_0:def 10; :: thesis: verum

end;

now

assume A23: (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)) ;
then (max- (f + g)) . x = - ((f . x) + (g . x)) by A8, XXREAL_0:def 10;
then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + (f . x)) + 0 by A9, A11, A19, 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 A7, A12, A19, A23, XXREAL_0:def 10; :: thesis: verum

end;

hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A20; :: thesis: verum

end;

hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A13; :: thesis: verum

end;

now

assume A24: 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) ;
then A25: (max- f) . x = - (f . x) by A9, XXREAL_0:def 10;

A26: now

assume A27: 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 ;
then A28: (max- g) . x = 0 by A9, XXREAL_0:def 10;
A29: (max+ g) . x = g . x by A9, A27, XXREAL_0:def 10;

A30: now

assume A31: 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 ;
then A32: (max- (f + g)) . x = 0 by A8, XXREAL_0:def 10;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + (- (f . x))) + 0 by A7, A25, A28, A31, 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 A9, A24, A29, A32, XXREAL_0:def 10; :: thesis: verum

end;

now

assume A33: (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)) ;
then (max- (f + g)) . x = - ((f . x) + (g . x)) by A8, XXREAL_0:def 10;
then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + 0 ) + (g . x) by A9, A24, A29, XXREAL_0:def 10
.= (- (f . x)) + ((- (g . x)) + (g . x)) ;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A7, A25, A28, A33, XXREAL_0:def 10; :: thesis: verum

end;

hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A30; :: thesis: verum

end;

now

assume A34: 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) ;
then A35: (max- g) . x = - (g . x) by A9, XXREAL_0:def 10;
A36: (f . x) + (g . x) <= 0 + 0 by A24, A34;
then - 0 <= - ((f . x) + (g . x)) ;
then A37: (max- (f + g)) . x = - ((f . x) + (g . x)) by A8, XXREAL_0:def 10;
A38: (max+ g) . x = 0 by A9, A34, XXREAL_0:def 10;
A39: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (0 + (- (f . x))) + (- (g . x)) by A7, A25, A35, A36, XXREAL_0:def 10;
(((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + 0 ) + 0 by A9, A24, A37, A38, 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 A39; :: thesis: verum

end;

hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A26; :: thesis: verum

end;

hence (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x by A4, A5, A10, Th60; :: thesis: verum

end;

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