let X1, X2 be non empty set ; 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
( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
let S1 be 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
( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
let S2 be 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
( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
let M1 be 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
( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
let M2 be 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
( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
let f be PartFunc of [:X1,X2:],ExtREAL; ( M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) implies ( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 ) )
assume that
A1:
M1 is sigma_finite
and
A2:
M2 is sigma_finite
and
A3:
f is_integrable_on Prod_Measure (M1,M2)
; ( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
set PM = 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 E -measurable & max- f is E -measurable & |.f.| is E -measurable )
by A4, MESFUNC2:27, MESFUN11:10;
A6:
( dom (max+ f) = E & dom (max- f) = E & dom |.f.| = E )
by A4, MESFUNC1:def 10, MESFUNC2:def 2, MESFUNC2:def 3;
A7:
( max+ f is nonnegative & max- f is nonnegative & |.f.| is nonnegative )
by MESFUN11:5;
then A8:
( Integral1 (M1,(max+ f)) is V97() & Integral2 (M2,(max+ f)) is V97() & Integral1 (M1,(max- f)) is V97() & Integral2 (M2,(max- f)) is V97() & Integral1 (M1,|.f.|) is V97() & Integral2 (M2,|.f.|) is V97() )
by A5, A6, MESFUN12:66;
A9:
( Integral1 (M1,(max+ f)) is XX2 -measurable & Integral1 (M1,(max- f)) is XX2 -measurable & Integral1 (M1,|.f.|) is XX2 -measurable & Integral2 (M2,(max+ f)) is XX1 -measurable & Integral2 (M2,(max- f)) is XX1 -measurable & Integral2 (M2,|.f.|) is XX1 -measurable )
by A1, A2, A5, A6, MESFUN11:5, MESFUN12:59, MESFUN12:60;
A10:
( dom (Integral1 (M1,(max+ f))) = XX2 & dom (Integral2 (M2,(max+ f))) = XX1 & dom (Integral1 (M1,(max- f))) = XX2 & dom (Integral2 (M2,(max- f))) = XX1 & dom (Integral1 (M1,|.f.|)) = XX2 & dom (Integral2 (M2,|.f.|)) = XX1 )
by FUNCT_2:def 1;
( 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 A5, A6, MESFUN11:5, MESFUNC5:88;
then
( 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 (M2,(Integral1 (M1,(max- f)))) & integral+ ((Prod_Measure (M1,M2)),(max- f)) = Integral (M1,(Integral2 (M2,(max- f)))) )
by A1, A2, A5, A6, A7, MESFUN12:84;
then A11:
( Integral (M2,(Integral1 (M1,(max+ f)))) < +infty & Integral (M1,(Integral2 (M2,(max+ f)))) < +infty & Integral (M2,(Integral1 (M1,(max- f)))) < +infty & Integral (M1,(Integral2 (M2,(max- f)))) < +infty )
by A3, MESFUNC5:def 17;
( Integral1 (M1,(max+ f)) = max+ (Integral1 (M1,(max+ f))) & Integral2 (M2,(max+ f)) = max+ (Integral2 (M2,(max+ f))) & Integral1 (M1,(max- f)) = max+ (Integral1 (M1,(max- f))) & Integral2 (M2,(max- f)) = max+ (Integral2 (M2,(max- f))) )
by A8, MESFUN11:31;
then A12:
( integral+ (M2,(max+ (Integral1 (M1,(max+ f))))) < +infty & integral+ (M1,(max+ (Integral2 (M2,(max+ f))))) < +infty & integral+ (M2,(max+ (Integral1 (M1,(max- f))))) < +infty & integral+ (M1,(max+ (Integral2 (M2,(max- f))))) < +infty )
by A8, A9, A10, A11, MESFUNC5:88;
( integral+ (M2,(max- (Integral1 (M1,(max+ f))))) = 0 & integral+ (M1,(max- (Integral2 (M2,(max+ f))))) = 0 & integral+ (M2,(max- (Integral1 (M1,(max- f))))) = 0 & integral+ (M1,(max- (Integral2 (M2,(max- f))))) = 0 )
by A8, A9, A10, MESFUN11:53;
hence
( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 )
by A9, A10, A12, MESFUNC5:def 17; ( Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
A13:
|.f.| is_integrable_on Prod_Measure (M1,M2)
by A3, A4, MESFUNC5:100;
max+ |.f.| = |.f.|
by MESFUN11:31;
then
integral+ ((Prod_Measure (M1,M2)),(max+ |.f.|)) = Integral ((Prod_Measure (M1,M2)),|.f.|)
by A6, A4, MESFUNC2:27, MESFUNC5:88;
then
( integral+ ((Prod_Measure (M1,M2)),(max+ |.f.|)) = Integral (M2,(Integral1 (M1,|.f.|))) & integral+ ((Prod_Measure (M1,M2)),(max+ |.f.|)) = Integral (M1,(Integral2 (M2,|.f.|))) )
by A1, A2, A5, A6, MESFUN12:84;
then A15:
( Integral (M2,(Integral1 (M1,|.f.|))) < +infty & Integral (M1,(Integral2 (M2,|.f.|))) < +infty )
by A13, MESFUNC5:def 17;
( Integral1 (M1,|.f.|) = max+ (Integral1 (M1,|.f.|)) & Integral2 (M2,|.f.|) = max+ (Integral2 (M2,|.f.|)) )
by A8, MESFUN11:31;
then A16:
( integral+ (M2,(max+ (Integral1 (M1,|.f.|)))) < +infty & integral+ (M1,(max+ (Integral2 (M2,|.f.|)))) < +infty )
by A8, A9, A10, A15, MESFUNC5:88;
( integral+ (M2,(max- (Integral1 (M1,|.f.|)))) = 0 & integral+ (M1,(max- (Integral2 (M2,|.f.|)))) = 0 )
by A8, A9, A10, MESFUN11:53;
hence
( Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
by A9, A10, A16, MESFUNC5:def 17; verum