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 ) )
proof
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 ) )
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: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;
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: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;
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 () 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