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 )
dom (f + g) = (dom f) /\ (dom g) by A1, A2, Th22;
then A3: ( dom (max+ (f + g)) = (dom f) /\ (dom g) & dom (max- (f + g)) = (dom f) /\ (dom g) ) by MESFUNC2:def 2, MESFUNC2:def 3;
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 A4: ( max+ (f + g) is without-infty & max- (f + g) is without-infty ) by Th16;
A5: ( 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 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 & max- f is without-infty & max+ g is without-infty & max- g is without-infty ) by Th16;
then ( 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 A4, Th22;
then A7: ( 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 A3, A5, 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 )
A8: 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 A9: 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 MESFUNC2:14, MESFUNC2:15;
then 0 <= ((max+ (f + g)) . x) + ((max- f) . x) ;
hence 0 <= ((max+ (f + g)) + (max- f)) . x by A9, MESFUNC1:def 3; :: thesis: verum

end;

assume A10: 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 MESFUNC2:14, MESFUNC2:15;
then 0 <= ((max- (f + g)) . x) + ((max+ f) . x) ;
hence 0 <= ((max- (f + g)) + (max+ f)) . x by A10, MESFUNC1:def 3; :: thesis: verum

end;

then 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 A11: ( (max+ (f + g)) + (max- f) is without-infty & (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 A5, A6, A7, 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 )
dom (((max- (f + g)) + (max+ f)) + (max+ g)) = ((dom f) /\ (dom g)) /\ (dom g) by A5, A6, A7, A11, 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 A8, SUPINF_2:71; :: thesis: verum