let X1, X2 be non empty set ; :: thesis:
let S1 be SigmaField of X1; :: thesis:
let S2 be SigmaField of X2; :: thesis:
let M1 be sigma_Measure of S1; :: thesis:
let M2 be sigma_Measure of S2; :: thesis:
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis:
let SX1 be Element of S1; :: thesis:
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_integrable_on Prod_Measure (M1,M2) and
A4: X1 = SX1 ; :: thesis:
consider A being Element of sigma (measurable_rectangles (S1,S2)) such that
A5: ( A = dom f & f is A -measurable ) by A3, MESFUNC5:def 17;
A6: ( A = dom |.f.| & A = dom (max+ f) & A = dom (max- f) ) by A5, MESFUNC1:def 10, MESFUNC2:def 2, MESFUNC2:def 3;
A7: ( |.f.| is A -measurable & max+ f is A -measurable & max- f is A -measurable ) by A5, MESFUNC2:25, MESFUNC2:26, MESFUNC2:27;
A8: ( Integral2 (M2,|.f.|) is_integrable_on M1 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral2 (M2,(max- f)) is_integrable_on M1 ) by A1, A2, A3, Th20;
A9: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;
Integral2 (M2,|.f.|) is_a.e.finite M1 by A8, Th19;
then consider U being Element of S1 such that
A10: ( M1 . U = 0 & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL ) ;
A11: U ` = SX1 \ U by A4, SUBSET_1:def 4;
then A12: ( (Integral2 (M2,|.f.|)) | (U `) is_integrable_on M1 & (Integral2 (M2,(max+ f))) | (U `) is_integrable_on M1 & (Integral2 (M2,(max- f))) | (U `) is_integrable_on M1 ) by A8, MESFUNC5:97;
A13: ( dom (Integral2 (M2,f)) = X1 & dom (Integral2 (M2,(max+ f))) = X1 & dom (Integral2 (M2,(max- f))) = X1 & dom (Integral2 (M2,|.f.|)) = X1 ) by FUNCT_2:def 1;
take U ; :: thesis:
thus M1 . U = 0 by A10; :: thesis:
thus A14: for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2 :: thesis:

proof

let x be Element of X1; :: thesis:
assume A15: x in U ` ; :: thesis:
then A16: x in dom ((Integral2 (M2,|.f.|)) | (U `)) by A13, RELAT_1:57;
X-section (A,x) = Measurable-X-section (A,x) by MEASUR11:def 6;
then A17: ( dom (ProjPMap1 (|.f.|,x)) = Measurable-X-section (A,x) & dom (ProjPMap1 (f,x)) = Measurable-X-section (A,x) ) by A5, A6, MESFUN12:def 3;
A18: ( ProjPMap1 (|.f.|,x) is Measurable-X-section (A,x) -measurable & ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable ) by A5, A6, A7, MESFUN12:47;
A19: ProjPMap1 (|.f.|,x) = |.(ProjPMap1 (f,x)).| by Th27;
then integral+ (M2,(max+ (ProjPMap1 (|.f.|,x)))) = integral+ (M2,(ProjPMap1 (|.f.|,x))) by MESFUN11:31
.= Integral (M2,(ProjPMap1 (|.f.|,x))) by A6, A7, A17, A19, MESFUN12:47, MESFUNC5:88
.= (Integral2 (M2,|.f.|)) . x by MESFUN12:def 8
.= ((Integral2 (M2,|.f.|)) | (U `)) . x by A15, FUNCT_1:49 ;
then A20: integral+ (M2,(max+ (ProjPMap1 (|.f.|,x)))) < +infty by A10, A16, PARTFUN1:4, XXREAL_0:9;
integral+ (M2,(max- (ProjPMap1 (|.f.|,x)))) < +infty by A17, A18, A19, MESFUN11:53;
then |.(ProjPMap1 (f,x)).| is_integrable_on M2 by A6, A7, A17, A19, A20, MESFUN12:47, MESFUNC5:def 17;
hence ProjPMap1 (f,x) is_integrable_on M2 by A17, A18, MESFUNC5:100; :: thesis:

end;

A22: now :: thesis:

let x be object ; :: thesis:

per cases ;

suppose A23: x in dom ((Integral2 (M2,(max+ f))) | (U `)) ; :: thesis:

then reconsider x1 = x as Element of X1 ;
A24: ((Integral2 (M2,(max+ f))) | (U `)) . x = (Integral2 (M2,(max+ f))) . x by A21, A23, FUNCT_1:49
.= Integral (M2,(ProjPMap1 ((max+ f),x1))) by MESFUN12:def 8
.= Integral (M2,(max+ (ProjPMap1 (f,x1)))) by MESFUN12:45 ;
A25: ProjPMap1 (f,x1) is_integrable_on M2 by A14, A21, A23;
then consider B being Element of S2 such that
A26: ( B = dom (ProjPMap1 (f,x1)) & ProjPMap1 (f,x1) is B -measurable ) by MESFUNC5:def 17;
A27: ( B = dom (max+ (ProjPMap1 (f,x1))) & max+ (ProjPMap1 (f,x1)) is B -measurable ) by A26, MESFUNC2:def 2, MESFUN11:10;
integral+ (M2,(max+ (ProjPMap1 (f,x1)))) < +infty by A25, MESFUNC5:def 17;
hence ((Integral2 (M2,(max+ f))) | (U `)) . x < +infty by A24, A27, MESFUNC5:88, MESFUN11:5; :: thesis:

end;

suppose not x in dom ((Integral2 (M2,(max+ f))) | (U `)) ; :: thesis:

hence ((Integral2 (M2,(max+ f))) | (U `)) . x < +infty by FUNCT_1:def 2; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:

per cases ;

suppose A28: x in dom ((Integral2 (M2,(max+ f))) | (U `)) ; :: thesis:

then reconsider x1 = x as Element of X1 ;
A29: ((Integral2 (M2,(max+ f))) | (U `)) . x = (Integral2 (M2,(max+ f))) . x by A21, A28, FUNCT_1:49
.= Integral (M2,(ProjPMap1 ((max+ f),x1))) by MESFUN12:def 8
.= Integral (M2,(max+ (ProjPMap1 (f,x1)))) by MESFUN12:45 ;
ProjPMap1 (f,x1) is_integrable_on M2 by A14, A21, A28;
then consider B being Element of S2 such that
A30: ( B = dom (ProjPMap1 (f,x1)) & ProjPMap1 (f,x1) is B -measurable ) by MESFUNC5:def 17;
( B = dom (max+ (ProjPMap1 (f,x1))) & max+ (ProjPMap1 (f,x1)) is B -measurable ) by A30, MESFUNC2:def 2, MESFUN11:10;
hence ((Integral2 (M2,(max+ f))) | (U `)) . x > -infty by A29, MESFUNC5:90, MESFUN11:5; :: thesis:

end;

suppose not x in dom ((Integral2 (M2,(max+ f))) | (U `)) ; :: thesis:

hence ((Integral2 (M2,(max+ f))) | (U `)) . x > -infty by FUNCT_1:def 2; :: thesis:

end;

then A31: ( (Integral2 (M2,(max+ f))) | (U `) is without-infty & (Integral2 (M2,(max+ f))) | (U `) is without+infty ) by A22, MESFUNC5:def 5, MESFUNC5:def 6;
then A32: dom G = (dom ((Integral2 (M2,(max+ f))) | (U `))) /\ (dom ((Integral2 (M2,(max- f))) | (U `))) by MESFUN11:23;
A33: ex A1 being Element of S1 st
( A1 = dom ((Integral2 (M2,(max+ f))) | (U `)) & (Integral2 (M2,(max+ f))) | (U `) is A1 -measurable ) by A12, MESFUNC5:def 17;
A34: ex A2 being Element of S1 st
( A2 = dom ((Integral2 (M2,(max- f))) | (U `)) & (Integral2 (M2,(max- f))) | (U `) is A2 -measurable ) by A12, MESFUNC5:def 17;

now :: thesis:

let x be object ; :: thesis:

per cases ;

suppose A35: x in dom ((Integral2 (M2,(max- f))) | (U `)) ; :: thesis:

then reconsider x1 = x as Element of X1 ;
A36: ((Integral2 (M2,(max- f))) | (U `)) . x = (Integral2 (M2,(max- f))) . x by A21, A35, FUNCT_1:49
.= Integral (M2,(ProjPMap1 ((max- f),x1))) by MESFUN12:def 8
.= Integral (M2,(max- (ProjPMap1 (f,x1)))) by MESFUN12:45 ;
ProjPMap1 (f,x1) is_integrable_on M2 by A14, A21, A35;
then consider B being Element of S2 such that
A37: ( B = dom (ProjPMap1 (f,x1)) & ProjPMap1 (f,x1) is B -measurable ) by MESFUNC5:def 17;
( B = dom (max- (ProjPMap1 (f,x1))) & max- (ProjPMap1 (f,x1)) is B -measurable ) by A37, MESFUNC2:def 3, MESFUN11:10;
hence ((Integral2 (M2,(max- f))) | (U `)) . x > -infty by A36, MESFUNC5:90, MESFUN11:5; :: thesis:

end;

suppose not x in dom ((Integral2 (M2,(max- f))) | (U `)) ; :: thesis:

hence ((Integral2 (M2,(max- f))) | (U `)) . x > -infty by FUNCT_1:def 2; :: thesis:

end;

then (Integral2 (M2,(max- f))) | (U `) is without-infty by MESFUNC5:def 5;
then A38: G is SX1 \ U -measurable by A11, A21, A31, A32, A33, A34, MEASUR11:66;
A39: ( dom ((Integral2 (M2,f)) | (U `)) = U ` & dom (G | (U `)) = U ` & dom ((Integral2 (M2,|.f.|)) | (U `)) = U ` ) by A13, A21, A32, RELAT_1:62;
then A40: ( U ` = dom (max+ ((Integral2 (M2,f)) | (U `))) & U ` = dom (max- ((Integral2 (M2,f)) | (U `))) ) by MESFUNC2:def 2, MESFUNC2:def 3;

A41: now :: thesis:

let x be Element of X1; :: thesis:
assume A42: x in dom ((Integral2 (M2,f)) | (U `)) ; :: thesis:
then A43: x in U ` by A13, RELAT_1:62;
then A44: ((Integral2 (M2,f)) | (U `)) . x = (Integral2 (M2,f)) . x by FUNCT_1:49
.= Integral (M2,(ProjPMap1 (f,x))) by MESFUN12:def 8 ;
X-section (A,x) = Measurable-X-section (A,x) by MEASUR11:def 6;
then B17: ( dom (ProjPMap1 (|.f.|,x)) = Measurable-X-section (A,x) & dom (ProjPMap1 (f,x)) = Measurable-X-section (A,x) ) by A5, A6, MESFUN12:def 3;
x in dom G by A21, A32, A42, RELAT_1:57;
then (G | (U `)) . x = (((Integral2 (M2,(max+ f))) | (U `)) . x) - (((Integral2 (M2,(max- f))) | (U `)) . x) by A21, A32, MESFUNC1:def 4
.= ((Integral2 (M2,(max+ f))) . x) - (((Integral2 (M2,(max- f))) | (U `)) . x) by A43, FUNCT_1:49
.= ((Integral2 (M2,(max+ f))) . x) - ((Integral2 (M2,(max- f))) . x) by A43, FUNCT_1:49
.= (Integral (M2,(ProjPMap1 ((max+ f),x)))) - ((Integral2 (M2,(max- f))) . x) by MESFUN12:def 8
.= (Integral (M2,(ProjPMap1 ((max+ f),x)))) - (Integral (M2,(ProjPMap1 ((max- f),x)))) by MESFUN12:def 8
.= (Integral (M2,(max+ (ProjPMap1 (f,x))))) - (Integral (M2,(ProjPMap1 ((max- f),x)))) by MESFUN12:45
.= (Integral (M2,(max+ (ProjPMap1 (f,x))))) - (Integral (M2,(max- (ProjPMap1 (f,x))))) by MESFUN12:45
.= Integral (M2,(ProjPMap1 (f,x))) by A5, B17, MESFUN12:47, MESFUN11:54 ;
hence ((Integral2 (M2,f)) | (U `)) . x = (G | (U `)) . x by A44; :: thesis:

end;

hence Integral2 (M2,f) is SX1 \ U -measurable by A11, A13, A21, A32, A38, A39, PARTFUN1:5, MESFUN12:36; :: thesis:
(Integral2 (M2,f)) | (U `) is SX1 \ U -measurable by A13, A21, A32, A38, A41, RELAT_1:62, PARTFUN1:5;
then A45: ( max+ ((Integral2 (M2,f)) | (U `)) is SX1 \ U -measurable & max- ((Integral2 (M2,f)) | (U `)) is SX1 \ U -measurable ) by A11, A39, MESFUNC2:25, MESFUNC2:26;

now :: thesis:

end;

then A50: rng ((Integral2 (M2,f)) | (U `)) c= REAL ;

now :: thesis:

end;

then A56: max+ ((Integral2 (M2,f)) | (U `)) is_integrable_on M1 by A11, A12, A39, A45, A40, MESFUNC5:102;

now :: thesis:

end;

then max- ((Integral2 (M2,f)) | (U `)) is_integrable_on M1 by A11, A12, A39, A45, A40, MESFUNC5:102;
then (max+ ((Integral2 (M2,f)) | (U `))) - (max- ((Integral2 (M2,f)) | (U `))) is_integrable_on M1 by A56, MESFUN10:12;
hence A62: (Integral2 (M2,f)) | (U `) is_integrable_on M1 by MESFUNC2:23; :: thesis:
reconsider F = (Integral2 (M2,f)) | (U `) as PartFunc of X1,REAL by A50, RELSET_1:6;
R_EAL F is_integrable_on M1 by A62, MESFUNC5:def 7;
then F is_integrable_on M1 by MESFUNC6:def 4;
then F in { f where f is PartFunc of X1,REAL : ex ND being Element of S1 st
( M1 . ND = 0 & dom f = ND ` & f is_integrable_on M1 ) } by A10, A39;
hence (Integral2 (M2,f)) | (U `) in L1_Functions M1 by LPSPACE1:def 8; :: thesis:
consider g1 being PartFunc of X1,ExtREAL such that
A64: ( dom g1 = dom (Integral2 (M2,(max+ f))) & g1 | (U `) = (Integral2 (M2,(max+ f))) | (U `) & g1 is_integrable_on M1 & Integral (M1,g1) = Integral (M1,((Integral2 (M2,(max+ f))) | (U `))) ) by A8, A10, A11, A13, Th23, MESFUNC5:97;
consider g2 being PartFunc of X1,ExtREAL such that
A65: ( dom g2 = dom (Integral2 (M2,(max- f))) & g2 | (U `) = (Integral2 (M2,(max- f))) | (U `) & g2 is_integrable_on M1 & Integral (M1,g2) = Integral (M1,((Integral2 (M2,(max- f))) | (U `))) ) by A8, A10, A11, A13, Th23, MESFUNC5:97;
consider g being PartFunc of X1,ExtREAL such that
A66: ( dom g = dom (Integral2 (M2,f)) & g | (U `) = (Integral2 (M2,f)) | (U `) & g is_integrable_on M1 & Integral (M1,g) = Integral (M1,((Integral2 (M2,f)) | (U `))) ) by A10, A13, A62, Th23;
reconsider g = g as Function of X1,ExtREAL by A13, A66, FUNCT_2:def 1;
A67: ( dom (g | (U `)) = (dom g) /\ (U `) & dom (g1 | (U `)) = (dom g1) /\ (U `) & dom (g2 | (U `)) = (dom g2) /\ (U `) ) by RELAT_1:61;

now :: thesis:

let x be Element of X1; :: thesis:
assume A72: x in dom (g2 | (U `)) ; :: thesis:
then A68: x in U ` by RELAT_1:57;
A69: ProjPMap1 (f,x) is_integrable_on M2 by A14, A72, RELAT_1:57;
then consider DP being Element of S2 such that
A70: ( DP = dom (ProjPMap1 (f,x)) & ProjPMap1 (f,x) is DP -measurable ) by MESFUNC5:def 17;
A71: ( DP = dom (max- (ProjPMap1 (f,x))) & max- (ProjPMap1 (f,x)) is DP -measurable ) by A70, MESFUNC2:def 3, MESFUNC2:26;
A73: max- (ProjPMap1 (f,x)) is nonnegative by MESFUN11:5;
A74: (g2 | (U `)) . x = (Integral2 (M2,(max- f))) . x by A65, A68, FUNCT_1:49
.= Integral (M2,(ProjPMap1 ((max- f),x))) by MESFUN12:def 8
.= Integral (M2,(max- (ProjPMap1 (f,x)))) by MESFUN12:45
.= integral+ (M2,(max- (ProjPMap1 (f,x)))) by A71, MESFUNC5:88, MESFUN11:5 ;
then (g2 | (U `)) . x < +infty by A69, MESFUNC5:def 17;
hence |.((g2 | (U `)) . x).| < +infty by A71, A73, A74, MESFUNC5:79, EXTREAL1:def 1; :: thesis:

end;

now :: thesis:

let x be Element of X1; :: thesis:
assume A79: x in dom (g | (U `)) ; :: thesis:
then A80: x in U ` by RELAT_1:57;
then A81: (g | (U `)) . x = (Integral2 (M2,f)) . x by A66, FUNCT_1:49;
ProjPMap1 (f,x) is_integrable_on M2 by A14, A79, RELAT_1:57;
then A82: ex A being Element of S2 st
( A = dom (ProjPMap1 (f,x)) & ProjPMap1 (f,x) is A -measurable ) by MESFUNC5:def 17;
( (Integral2 (M2,(max+ f))) . x = Integral (M2,(ProjPMap1 ((max+ f),x))) & (Integral2 (M2,(max- f))) . x = Integral (M2,(ProjPMap1 ((max- f),x))) ) by MESFUN12:def 8;
then ( (Integral2 (M2,(max+ f))) . x = Integral (M2,(max+ (ProjPMap1 (f,x)))) & (Integral2 (M2,(max- f))) . x = Integral (M2,(max- (ProjPMap1 (f,x)))) ) by MESFUN12:45;
then ((Integral2 (M2,(max+ f))) . x) - ((Integral2 (M2,(max- f))) . x) = Integral (M2,(ProjPMap1 (f,x))) by A82, MESFUN11:54
.= (Integral2 (M2,f)) . x by MESFUN12:def 8 ;
then (g | (U `)) . x = (((Integral2 (M2,(max+ f))) | (U `)) . x) - ((Integral2 (M2,(max- f))) . x) by A80, A81, FUNCT_1:49
.= ((g1 | (U `)) . x) - ((g2 | (U `)) . x) by A64, A65, A80, FUNCT_1:49 ;
hence (g | (U `)) . x = ((g1 | (U `)) - (g2 | (U `))) . x by A76, A79, MESFUNC1:def 4; :: thesis:

end;

then A83: g | (U `) = (g1 | (U `)) - (g2 | (U `)) by A13, A64, A65, A66, A75, RELAT_1:61, PARTFUN1:5;
A84: ( Integral2 (M2,(max+ f)) is SX1 -measurable & Integral2 (M2,(max- f)) is SX1 -measurable ) by A2, A6, A7, MESFUN11:5, MESFUN12:60;
A85: Integral ((Prod_Measure (M1,M2)),(max+ f)) = Integral (M1,(Integral2 (M2,(max+ f)))) by A1, A2, A6, A7, A9, MESFUN12:84
.= Integral (M1,((Integral2 (M2,(max+ f))) | (SX1 \ U))) by A4, A10, A13, A84, MESFUNC5:95
.= Integral (M1,(g1 | (U `))) by A4, A64, SUBSET_1:def 4 ;
A86: Integral ((Prod_Measure (M1,M2)),(max- f)) = Integral (M1,(Integral2 (M2,(max- f)))) by A1, A2, A6, A7, A9, MESFUN12:84
.= Integral (M1,((Integral2 (M2,(max- f))) | (SX1 \ U))) by A4, A10, A13, A84, MESFUNC5:95
.= Integral (M1,(g2 | (U `))) by A4, A65, SUBSET_1:def 4 ;
Integral ((Prod_Measure (M1,M2)),f) = (Integral (M1,((g1 | (U `)) | (U `)))) - (Integral (M1,((g2 | (U `)) | (U `)))) by A5, A85, A86, MESFUN11:54;
then Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(g | (U `))) by A77, A78, A83, Th21;
hence ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) by A66; :: thesis: