let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st f is () & g is () 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 () & g is () 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 () and

A2: g is () ; :: 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, Th16;

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:12, MESFUNC2:13;

then A6: max+ f is () by Th10;

A7: max- f is () by A5, Th10;

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:12, MESFUNC2:13;

then max+ (f + g) is () by Th10;

then A9: dom ((max+ (f + g)) + (max- f)) = (dom (max+ (f + g))) /\ (dom (max- f)) by A7, Th16;

max- (f + g) is () by A8, Th10;

then A10: dom ((max- (f + g)) + (max+ f)) = (dom (max- (f + g))) /\ (dom (max+ f)) by A6, Th16;

A11: max- g is () by A5, Th10;

A12: dom (max- f) = dom f by MESFUNC2:def 3;

A13: max+ g is () by A5, Th10;

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 object 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 ) )

( ( 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 () by Th10;

then dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom f) /\ (dom g)) /\ (dom g) by A14, A11, A17, Th16

.= (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 () by A24, Th10;

then dom (((max- (f + g)) + (max+ f)) + (max+ g)) = ((dom f) /\ (dom g)) /\ (dom g) by A18, A13, A16, Th16;

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:52; :: thesis: verum

( 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 () & g is () 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 () and

A2: g is () ; :: 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, Th16;

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:12, MESFUNC2:13;

then A6: max+ f is () by Th10;

A7: max- f is () by A5, Th10;

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:12, MESFUNC2:13;

then max+ (f + g) is () by Th10;

then A9: dom ((max+ (f + g)) + (max- f)) = (dom (max+ (f + g))) /\ (dom (max- f)) by A7, Th16;

max- (f + g) is () by A8, Th10;

then A10: dom ((max- (f + g)) + (max+ f)) = (dom (max- (f + g))) /\ (dom (max+ f)) by A6, Th16;

A11: max- g is () by A5, Th10;

A12: dom (max- f) = dom f by MESFUNC2:def 3;

A13: max+ g is () by A5, Th10;

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 object 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

then A24:
for x being set holds
let x be object ; :: 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 ) )

then A23: 0 <= (max+ f) . x by MESFUNC2:12;

0 <= (max- (f + g)) . x by A22, MESFUNC2:13;

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;hereby :: thesis: ( x in dom ((max- (f + g)) + (max+ f)) implies 0 <= ((max- (f + g)) + (max+ f)) . x )

assume A22:
x in dom ((max- (f + g)) + (max+ f))
; :: thesis: 0 <= ((max- (f + g)) + (max+ f)) . xassume 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:13;

0 <= (max+ (f + g)) . x by A20, MESFUNC2:12;

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;then A21: 0 <= (max- f) . x by MESFUNC2:13;

0 <= (max+ (f + g)) . x by A20, MESFUNC2:12;

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

then A23: 0 <= (max+ f) . x by MESFUNC2:12;

0 <= (max- (f + g)) . x by A22, MESFUNC2:13;

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

( ( 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 () by Th10;

then dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom f) /\ (dom g)) /\ (dom g) by A14, A11, A17, Th16

.= (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 () by A24, Th10;

then dom (((max- (f + g)) + (max+ f)) + (max+ g)) = ((dom f) /\ (dom g)) /\ (dom g) by A18, A13, A16, Th16;

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:52; :: thesis: verum