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 nonnegative & 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))))) & Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) & Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) )
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 nonnegative & 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))))) & Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) & Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) )
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 nonnegative & 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))))) & Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) & Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) )
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 nonnegative & 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))))) & Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) & Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) )
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 nonnegative & 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))))) & Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) & Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) )
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 nonnegative & 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))))) & Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) & Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) )
let A, B be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( A = dom f & f is nonnegative & 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))))) & Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) & Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) ) )
assume that
A1: A = dom f and
A2: f is nonnegative 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))))) & Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) & Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) )
reconsider g1 = - g as nonnegative PartFunc of [:X1,X2:],ExtREAL by A5;
A7: B = dom g1 by A4, MESFUNC1:def 7;
A8: g1 is B -measurable by A4, A6, MEASUR11:63;
A9: ( f is A /\ B -measurable & g is A /\ B -measurable ) by A3, A6, XBOOLE_1:17, MESFUNC1:30;
A10: dom (f - g) = A /\ B by A1, A2, A4, A5, MESFUNC5:17;
then A11: A /\ B = dom (g | (dom (f - g))) by A4, XBOOLE_1:17, RELAT_1:62;
then A /\ B = (dom g) /\ (dom (f - g)) by RELAT_1:61;
then A12: g | (dom (f - g)) is A /\ B -measurable by A9, A10, MESFUNC5:42;
A13: f + g1 = f - g by MESFUNC2:8;
then A14: Integral1 (M1,(f - g)) = (Integral1 (M1,(f | (dom (f - g))))) + (Integral1 (M1,(g1 | (dom (f - g))))) by A1, A2, A3, A7, A8, Th74
.= (Integral1 (M1,(f | (dom (f - g))))) + (Integral1 (M1,(- (g | (dom (f - g)))))) by MESFUN11:3
.= (Integral1 (M1,(f | (dom (f - g))))) + (- (Integral1 (M1,(g | (dom (f - g)))))) by A11, A12, Th73 ;
hence Integral1 (M1,(f - g)) = (Integral1 (M1,(f | (dom (f - g))))) - (Integral1 (M1,(g | (dom (f - g))))) by MESFUNC2:8; :: thesis: ( Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) & Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) )
A15: f - g is A /\ B -measurable by A2, A5, A9, A10, MEASUR11:67;
A16: g - f = - (f - g) by MEASUR11:64;
then A17: dom (g - f) = A /\ B by A10, MESFUNC1:def 7;
Integral1 (M1,(g - f)) = - (Integral1 (M1,(f - g))) by A10, A16, A15, Th73;
hence Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) by A10, A14, A17, MEASUR11:64; :: thesis: ( Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) )
A18: Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) + (Integral2 (M2,(g1 | (dom (f - g))))) by A1, A2, A3, A7, A8, A13, Th74
.= (Integral2 (M2,(f | (dom (f - g))))) + (Integral2 (M2,(- (g | (dom (f - g)))))) by MESFUN11:3
.= (Integral2 (M2,(f | (dom (f - g))))) + (- (Integral2 (M2,(g | (dom (f - g)))))) by A11, A12, Th73 ;
hence Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) by MESFUNC2:8; :: thesis: Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f)))))
Integral2 (M2,(g - f)) = - (Integral2 (M2,(f - g))) by A10, A16, A15, Th73;
hence Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) by A10, A18, A17, MEASUR11:64; :: thesis: verum