let X be non empty set ; :: thesis: for f, g being PartFunc of X, REAL holds
( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
let f, g be PartFunc of X, REAL ; :: thesis: ( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then A1: ( dom (max+ (f + g)) = (dom f) /\ (dom g) & dom (max- (f + g)) = (dom f) /\ (dom g) ) by RFUNCT_3:def 10, RFUNCT_3:def 11;
A2: ( 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)) = (dom (max+ (f + g))) /\ (dom (max- f)) & dom ((max- (f + g)) + (max+ f)) = (dom (max- (f + g))) /\ (dom (max+ f)) ) by VALUED_1:def 1;
then A3: ( dom ((max+ (f + g)) + (max- f)) = (dom g) /\ ((dom f) /\ (dom f)) & dom ((max- (f + g)) + (max+ f)) = (dom g) /\ ((dom f) /\ (dom f)) ) by A1, A2, XBOOLE_1:16;
hence ( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) ) ; :: thesis: ( dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom f) /\ (dom g)) /\ (dom g) by A2, A3, VALUED_1:def 1
.= (dom f) /\ ((dom g) /\ (dom g)) by XBOOLE_1:16 ;
hence dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) ; :: thesis: ( dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
dom (((max- (f + g)) + (max+ f)) + (max+ g)) = ((dom f) /\ (dom g)) /\ (dom g) by A2, A3, VALUED_1:def 1;
then dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ ((dom g) /\ (dom g)) by XBOOLE_1:16;
hence dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) ; :: thesis: ( (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )

now

let x be set ; :: thesis: ( x in dom ((max+ (f + g)) + (max- f)) implies 0 <= ((max+ (f + g)) + (max- f)) . x )
assume A4: x in dom ((max+ (f + g)) + (max- f)) ; :: thesis: 0 <= ((max+ (f + g)) + (max- f)) . x
then ( 0 <= (max+ (f + g)) . x & 0 <= (max- f) . x ) by RFUNCT_3:40, RFUNCT_3:43;
then 0 + 0 <= ((max+ (f + g)) . x) + ((max- f) . x) ;
hence 0 <= ((max+ (f + g)) + (max- f)) . x by A4, VALUED_1:def 1; :: thesis: verum

end;

hence (max+ (f + g)) + (max- f) is nonnegative by Th52; :: thesis: (max- (f + g)) + (max+ f) is nonnegative

now

let x be set ; :: thesis: ( x in dom ((max- (f + g)) + (max+ f)) implies 0 <= ((max- (f + g)) + (max+ f)) . x )
assume A5: x in dom ((max- (f + g)) + (max+ f)) ; :: thesis: 0 <= ((max- (f + g)) + (max+ f)) . x
then ( 0 <= (max- (f + g)) . x & 0 <= (max+ f) . x ) by RFUNCT_3:40, RFUNCT_3:43;
then 0 + 0 <= ((max- (f + g)) . x) + ((max+ f) . x) ;
hence 0 <= ((max- (f + g)) + (max+ f)) . x by A5, VALUED_1:def 1; :: thesis: verum

end;

hence (max- (f + g)) + (max+ f) is nonnegative by Th52; :: thesis: verum