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 being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) holds
( Integral ((Prod_Measure (M1,M2)),f) = (Integral (M2,(Integral1 (M1,(max+ f))))) - (Integral (M2,(Integral1 (M1,(max- f))))) & Integral ((Prod_Measure (M1,M2)),f) = (Integral (M1,(Integral2 (M2,(max+ f))))) - (Integral (M1,(Integral2 (M2,(max- 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 being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) holds
( Integral ((Prod_Measure (M1,M2)),f) = (Integral (M2,(Integral1 (M1,(max+ f))))) - (Integral (M2,(Integral1 (M1,(max- f))))) & Integral ((Prod_Measure (M1,M2)),f) = (Integral (M1,(Integral2 (M2,(max+ f))))) - (Integral (M1,(Integral2 (M2,(max- f))))) )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) holds
( Integral ((Prod_Measure (M1,M2)),f) = (Integral (M2,(Integral1 (M1,(max+ f))))) - (Integral (M2,(Integral1 (M1,(max- f))))) & Integral ((Prod_Measure (M1,M2)),f) = (Integral (M1,(Integral2 (M2,(max+ f))))) - (Integral (M1,(Integral2 (M2,(max- f))))) )
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) holds
( Integral ((Prod_Measure (M1,M2)),f) = (Integral (M2,(Integral1 (M1,(max+ f))))) - (Integral (M2,(Integral1 (M1,(max- f))))) & Integral ((Prod_Measure (M1,M2)),f) = (Integral (M1,(Integral2 (M2,(max+ f))))) - (Integral (M1,(Integral2 (M2,(max- f))))) )
let M2 be sigma_Measure of S2; :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) holds
( Integral ((Prod_Measure (M1,M2)),f) = (Integral (M2,(Integral1 (M1,(max+ f))))) - (Integral (M2,(Integral1 (M1,(max- f))))) & Integral ((Prod_Measure (M1,M2)),f) = (Integral (M1,(Integral2 (M2,(max+ f))))) - (Integral (M1,(Integral2 (M2,(max- f))))) )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: ( M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) implies ( Integral ((Prod_Measure (M1,M2)),f) = (Integral (M2,(Integral1 (M1,(max+ f))))) - (Integral (M2,(Integral1 (M1,(max- f))))) & Integral ((Prod_Measure (M1,M2)),f) = (Integral (M1,(Integral2 (M2,(max+ f))))) - (Integral (M1,(Integral2 (M2,(max- f))))) ) )
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_integrable_on Prod_Measure (M1,M2) ; :: thesis: ( Integral ((Prod_Measure (M1,M2)),f) = (Integral (M2,(Integral1 (M1,(max+ f))))) - (Integral (M2,(Integral1 (M1,(max- f))))) & Integral ((Prod_Measure (M1,M2)),f) = (Integral (M1,(Integral2 (M2,(max+ f))))) - (Integral (M1,(Integral2 (M2,(max- f))))) )
set M = Prod_Measure (M1,M2);
consider E being Element of sigma (measurable_rectangles (S1,S2)) such that
A4: ( E = dom f & f is E -measurable ) by A3, MESFUNC5:def 17;
A5: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;
A6: ( dom (max+ f) = E & dom (max- f) = E ) by A4, MESFUNC2:def 2, MESFUNC2:def 3;
( max+ f is E -measurable & max- f is E -measurable ) by A4, MESFUNC2:25, MESFUNC2:26;
then A7: ( Integral ((Prod_Measure (M1,M2)),(max+ f)) = Integral (M2,(Integral1 (M1,(max+ f)))) & Integral ((Prod_Measure (M1,M2)),(max- f)) = Integral (M2,(Integral1 (M1,(max- f)))) & Integral ((Prod_Measure (M1,M2)),(max+ f)) = Integral (M1,(Integral2 (M2,(max+ f)))) & Integral ((Prod_Measure (M1,M2)),(max- f)) = Integral (M1,(Integral2 (M2,(max- f)))) ) by A1, A2, A5, A6, MESFUN12:84;
( integral+ ((Prod_Measure (M1,M2)),(max+ f)) = Integral ((Prod_Measure (M1,M2)),(max+ f)) & integral+ ((Prod_Measure (M1,M2)),(max- f)) = Integral ((Prod_Measure (M1,M2)),(max- f)) ) by A4, A5, A6, MESFUNC2:25, MESFUNC2:26, MESFUNC5:88;
hence ( Integral ((Prod_Measure (M1,M2)),f) = (Integral (M2,(Integral1 (M1,(max+ f))))) - (Integral (M2,(Integral1 (M1,(max- f))))) & Integral ((Prod_Measure (M1,M2)),f) = (Integral (M1,(Integral2 (M2,(max+ f))))) - (Integral (M1,(Integral2 (M2,(max- f))))) ) by A7, MESFUNC5:def 16; :: thesis: verum