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

proof

let x be set ; :: thesis: ( ( x in dom ((max+ (f + g)) + (max- f)) implies 0 <= ((max+ (f + g)) + (max- f)) . x ) & ( x in dom ((max- (f + g)) + (max+ f)) implies 0 <= ((max- (f + g)) + (max+ f)) . x ) )

hereby :: thesis: ( x in dom ((max- (f + g)) + (max+ f)) implies 0 <= ((max- (f + g)) + (max+ f)) . x )

assume A20: x in dom ((max+ (f + g)) + (max- f)) ; :: thesis: 0 <= ((max+ (f + g)) + (max- f)) . x
then A21: 0 <= (max- f) . x by MESFUNC2:15;
0 <= (max+ (f + g)) . x by A20, MESFUNC2:14;
then 0 <= ((max+ (f + g)) . x) + ((max- f) . x) by A21;
hence 0 <= ((max+ (f + g)) + (max- f)) . x by A20, MESFUNC1:def 3; :: thesis: verum

end;

assume A22: x in dom ((max- (f + g)) + (max+ f)) ; :: thesis: 0 <= ((max- (f + g)) + (max+ f)) . x
then A23: 0 <= (max+ f) . x by MESFUNC2:14;
0 <= (max- (f + g)) . x by A22, MESFUNC2:15;
then 0 <= ((max- (f + g)) . x) + ((max+ f) . x) by A23;
hence 0 <= ((max- (f + g)) + (max+ f)) . x by A22, MESFUNC1:def 3; :: thesis: verum

end;

then A24: for x being set holds
( ( x in dom ((max+ (f + g)) + (max- f)) implies -infty < ((max+ (f + g)) + (max- f)) . x ) & ( x in dom ((max- (f + g)) + (max+ f)) implies -infty < ((max- (f + g)) + (max+ f)) . x ) ) ;
then (max+ (f + g)) + (max- f) is without-infty by Th16;
then dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom f) /\ (dom g)) /\ (dom g) by A14, A11, A17, Th22
.= (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 )
(max- (f + g)) + (max+ f) is without-infty by A24, Th16;
then dom (((max- (f + g)) + (max+ f)) + (max+ g)) = ((dom f) /\ (dom g)) /\ (dom g) by A18, A13, A16, Th22;
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 )
thus ( (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative ) by A19, SUPINF_2:71; :: thesis: verum