let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f, g being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f, g being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f, g being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for f, g being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )
let M2 be sigma_Measure of S2; :: thesis: for f, g being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )
let f, g be PartFunc of [:X1,X2:],ExtREAL; :: thesis: for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )
let A, B be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( A = dom f & f is nonpositive & f is A -measurable & B = dom g & g is nonpositive & g is B -measurable implies ( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) ) )
assume that
A1: A = dom f and
A2: f is nonpositive and
A3: f is A -measurable and
A4: B = dom g and
A5: g is nonpositive and
A6: g is B -measurable ; :: thesis: ( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )
reconsider f1 = - f as nonnegative PartFunc of [:X1,X2:],ExtREAL by A2;
reconsider g1 = - g as nonnegative PartFunc of [:X1,X2:],ExtREAL by A5;
A7: f1 + g1 = - (f + g) by MEASUR11:64;
A8: ( dom f1 = A & dom g1 = B ) by A1, A4, MESFUNC1:def 7;
then A9: dom (f1 + g1) = A /\ B by MESFUNC5:22;
then A10: dom (f + g) = A /\ B by A7, MESFUNC1:def 7;
then A11: ( dom (f | (dom (f + g))) = A /\ B & dom (g | (dom (f + g))) = A /\ B ) by A1, A4, XBOOLE_1:17, RELAT_1:62;
A12: ( (dom f) /\ (A /\ B) = A /\ B & (dom g) /\ (A /\ B) = A /\ B ) by A1, A4, XBOOLE_1:17, XBOOLE_1:28;
A13: ( f1 | (dom (f1 + g1)) = - (f | (dom (f + g))) & g1 | (dom (f1 + g1)) = - (g | (dom (f + g))) ) by A9, A10, MESFUN11:3;
A14: ( f is A /\ B -measurable & g is A /\ B -measurable ) by A3, A6, XBOOLE_1:17, MESFUNC1:30;
then ( f | (dom (f + g)) is A /\ B -measurable & g | (dom (f + g)) is A /\ B -measurable ) by A10, A12, MESFUNC5:42;
then A15: ( Integral1 (M1,(f1 | (dom (f1 + g1)))) = - (Integral1 (M1,(f | (dom (f + g))))) & Integral1 (M1,(g1 | (dom (f1 + g1)))) = - (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f1 | (dom (f1 + g1)))) = - (Integral2 (M2,(f | (dom (f + g))))) & Integral2 (M2,(g1 | (dom (f1 + g1)))) = - (Integral2 (M2,(g | (dom (f + g))))) ) by A11, A13, Th73;
f + g is A /\ B -measurable by A2, A5, A10, A14, MEASUR11:65;
then A16: ( Integral1 (M1,(f1 + g1)) = - (Integral1 (M1,(f + g))) & Integral2 (M2,(f1 + g1)) = - (Integral2 (M2,(f + g))) ) by A7, A10, Th73;
A17: ( f1 is A -measurable & g1 is B -measurable ) by A1, A3, A4, A6, MEASUR11:63;
then Integral1 (M1,(f1 + g1)) = (Integral1 (M1,(f1 | (dom (f1 + g1))))) + (Integral1 (M1,(g1 | (dom (f1 + g1))))) by A8, Th74;
then - (Integral1 (M1,(f + g))) = - ((Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g)))))) by A15, A16, MEASUR11:64;
then Integral1 (M1,(f + g)) = - (- ((Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))))) by DBLSEQ_3:2;
hence Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) by DBLSEQ_3:2; :: thesis: Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g)))))
Integral2 (M2,(f1 + g1)) = (Integral2 (M2,(f1 | (dom (f1 + g1))))) + (Integral2 (M2,(g1 | (dom (f1 + g1))))) by A8, A17, Th74;
then - (Integral2 (M2,(f + g))) = - ((Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g)))))) by A15, A16, MEASUR11:64;
then Integral2 (M2,(f + g)) = - (- ((Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))))) by DBLSEQ_3:2;
hence Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) by DBLSEQ_3:2; :: thesis: verum