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 SX2 be Element of S2; :: 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: X2 = SX2 ; :: 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: ( Integral1 (M1,|.f.|) is_integrable_on M2 & Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral1 (M1,(max- f)) is_integrable_on M2 ) by A1, A2, A3, Th20;
A9: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;
Integral1 (M1,|.f.|) is_a.e.finite M2 by A8, Th19;
then consider V being Element of S2 such that
A10: ( M2 . V = 0 & (Integral1 (M1,|.f.|)) | (V `) is PartFunc of X2,REAL ) ;
A11: V ` = SX2 \ V by A4, SUBSET_1:def 4;
then A12: ( (Integral1 (M1,|.f.|)) | (V `) is_integrable_on M2 & (Integral1 (M1,(max+ f))) | (V `) is_integrable_on M2 & (Integral1 (M1,(max- f))) | (V `) is_integrable_on M2 ) by A8, MESFUNC5:97;
A13: ( dom (Integral1 (M1,f)) = X2 & dom (Integral1 (M1,(max+ f))) = X2 & dom (Integral1 (M1,(max- f))) = X2 & dom (Integral1 (M1,|.f.|)) = X2 ) by FUNCT_2:def 1;
take V ; :: thesis:
thus M2 . V = 0 by A10; :: thesis:
thus A14: for y being Element of X2 st y in V ` holds
ProjPMap2 (f,y) is_integrable_on M1 :: thesis:

proof

let y be Element of X2; :: thesis:
assume A15: y in V ` ; :: thesis:
then A16: y in dom ((Integral1 (M1,|.f.|)) | (V `)) by A13, RELAT_1:57;
Y-section (A,y) = Measurable-Y-section (A,y) by MEASUR11:def 7;
then A17: ( dom (ProjPMap2 (|.f.|,y)) = Measurable-Y-section (A,y) & dom (ProjPMap2 (f,y)) = Measurable-Y-section (A,y) ) by A5, A6, MESFUN12:def 4;
A18: ( ProjPMap2 (|.f.|,y) is Measurable-Y-section (A,y) -measurable & ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable ) by A5, A6, A7, MESFUN12:47;
A19: ProjPMap2 (|.f.|,y) = |.(ProjPMap2 (f,y)).| by Th27;
then integral+ (M1,(max+ (ProjPMap2 (|.f.|,y)))) = integral+ (M1,(ProjPMap2 (|.f.|,y))) by MESFUN11:31
.= Integral (M1,(ProjPMap2 (|.f.|,y))) by A6, A7, A17, A19, MESFUN12:47, MESFUNC5:88
.= (Integral1 (M1,|.f.|)) . y by MESFUN12:def 7
.= ((Integral1 (M1,|.f.|)) | (V `)) . y by A15, FUNCT_1:49 ;
then A20: integral+ (M1,(max+ (ProjPMap2 (|.f.|,y)))) < +infty by A10, A16, PARTFUN1:4, XXREAL_0:9;
integral+ (M1,(max- (ProjPMap2 (|.f.|,y)))) < +infty by A17, A18, A19, MESFUN11:53;
then |.(ProjPMap2 (f,y)).| is_integrable_on M1 by A6, A7, A17, A19, A20, MESFUN12:47, MESFUNC5:def 17;
hence ProjPMap2 (f,y) is_integrable_on M1 by A17, A18, MESFUNC5:100; :: thesis:

end;

A22: now :: thesis:

let x be object ; :: thesis:

per cases ;

suppose A23: x in dom ((Integral1 (M1,(max+ f))) | (V `)) ; :: thesis:

then reconsider x1 = x as Element of X2 ;
A24: ((Integral1 (M1,(max+ f))) | (V `)) . x = (Integral1 (M1,(max+ f))) . x by A21, A23, FUNCT_1:49
.= Integral (M1,(ProjPMap2 ((max+ f),x1))) by MESFUN12:def 7
.= Integral (M1,(max+ (ProjPMap2 (f,x1)))) by MESFUN12:46 ;
A25: ProjPMap2 (f,x1) is_integrable_on M1 by A14, A21, A23;
then consider B being Element of S1 such that
A26: ( B = dom (ProjPMap2 (f,x1)) & ProjPMap2 (f,x1) is B -measurable ) by MESFUNC5:def 17;
A27: ( B = dom (max+ (ProjPMap2 (f,x1))) & max+ (ProjPMap2 (f,x1)) is B -measurable ) by A26, MESFUNC2:def 2, MESFUN11:10;
integral+ (M1,(max+ (ProjPMap2 (f,x1)))) < +infty by A25, MESFUNC5:def 17;
hence ((Integral1 (M1,(max+ f))) | (V `)) . x < +infty by A24, A27, MESFUNC5:88, MESFUN11:5; :: thesis:

end;

suppose not x in dom ((Integral1 (M1,(max+ f))) | (V `)) ; :: thesis:

hence ((Integral1 (M1,(max+ f))) | (V `)) . x < +infty by FUNCT_1:def 2; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:

per cases ;

suppose A28: x in dom ((Integral1 (M1,(max+ f))) | (V `)) ; :: thesis:

then reconsider x1 = x as Element of X2 ;
A29: ((Integral1 (M1,(max+ f))) | (V `)) . x = (Integral1 (M1,(max+ f))) . x by A21, A28, FUNCT_1:49
.= Integral (M1,(ProjPMap2 ((max+ f),x1))) by MESFUN12:def 7
.= Integral (M1,(max+ (ProjPMap2 (f,x1)))) by MESFUN12:46 ;
ProjPMap2 (f,x1) is_integrable_on M1 by A14, A21, A28;
then consider B being Element of S1 such that
A30: ( B = dom (ProjPMap2 (f,x1)) & ProjPMap2 (f,x1) is B -measurable ) by MESFUNC5:def 17;
( B = dom (max+ (ProjPMap2 (f,x1))) & max+ (ProjPMap2 (f,x1)) is B -measurable ) by A30, MESFUNC2:def 2, MESFUN11:10;
hence ((Integral1 (M1,(max+ f))) | (V `)) . x > -infty by A29, MESFUNC5:90, MESFUN11:5; :: thesis:

end;

suppose not x in dom ((Integral1 (M1,(max+ f))) | (V `)) ; :: thesis:

hence ((Integral1 (M1,(max+ f))) | (V `)) . x > -infty by FUNCT_1:def 2; :: thesis:

end;

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

now :: thesis:

let x be object ; :: thesis:

per cases ;

suppose A35: x in dom ((Integral1 (M1,(max- f))) | (V `)) ; :: thesis:

then reconsider x1 = x as Element of X2 ;
A36: ((Integral1 (M1,(max- f))) | (V `)) . x = (Integral1 (M1,(max- f))) . x by A21, A35, FUNCT_1:49
.= Integral (M1,(ProjPMap2 ((max- f),x1))) by MESFUN12:def 7
.= Integral (M1,(max- (ProjPMap2 (f,x1)))) by MESFUN12:46 ;
ProjPMap2 (f,x1) is_integrable_on M1 by A14, A21, A35;
then consider B being Element of S1 such that
A37: ( B = dom (ProjPMap2 (f,x1)) & ProjPMap2 (f,x1) is B -measurable ) by MESFUNC5:def 17;
( B = dom (max- (ProjPMap2 (f,x1))) & max- (ProjPMap2 (f,x1)) is B -measurable ) by A37, MESFUNC2:def 3, MESFUN11:10;
hence ((Integral1 (M1,(max- f))) | (V `)) . x > -infty by A36, MESFUNC5:90, MESFUN11:5; :: thesis:

end;

suppose not x in dom ((Integral1 (M1,(max- f))) | (V `)) ; :: thesis:

hence ((Integral1 (M1,(max- f))) | (V `)) . x > -infty by FUNCT_1:def 2; :: thesis:

end;

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

A41: now :: thesis:

let x be Element of X2; :: thesis:
assume A42: x in dom ((Integral1 (M1,f)) | (V `)) ; :: thesis:
then A43: x in V ` by A13, RELAT_1:62;
then A44: ((Integral1 (M1,f)) | (V `)) . x = (Integral1 (M1,f)) . x by FUNCT_1:49
.= Integral (M1,(ProjPMap2 (f,x))) by MESFUN12:def 7 ;
Y-section (A,x) = Measurable-Y-section (A,x) by MEASUR11:def 7;
then B17: ( dom (ProjPMap2 (|.f.|,x)) = Measurable-Y-section (A,x) & dom (ProjPMap2 (f,x)) = Measurable-Y-section (A,x) ) by A5, A6, MESFUN12:def 4;
x in dom G by A21, A32, A42, RELAT_1:57;
then (G | (V `)) . x = (((Integral1 (M1,(max+ f))) | (V `)) . x) - (((Integral1 (M1,(max- f))) | (V `)) . x) by A21, A32, MESFUNC1:def 4
.= ((Integral1 (M1,(max+ f))) . x) - (((Integral1 (M1,(max- f))) | (V `)) . x) by A43, FUNCT_1:49
.= ((Integral1 (M1,(max+ f))) . x) - ((Integral1 (M1,(max- f))) . x) by A43, FUNCT_1:49
.= (Integral (M1,(ProjPMap2 ((max+ f),x)))) - ((Integral1 (M1,(max- f))) . x) by MESFUN12:def 7
.= (Integral (M1,(ProjPMap2 ((max+ f),x)))) - (Integral (M1,(ProjPMap2 ((max- f),x)))) by MESFUN12:def 7
.= (Integral (M1,(max+ (ProjPMap2 (f,x))))) - (Integral (M1,(ProjPMap2 ((max- f),x)))) by MESFUN12:46
.= (Integral (M1,(max+ (ProjPMap2 (f,x))))) - (Integral (M1,(max- (ProjPMap2 (f,x))))) by MESFUN12:46
.= Integral (M1,(ProjPMap2 (f,x))) by A5, B17, MESFUN12:47, MESFUN11:54 ;
hence ((Integral1 (M1,f)) | (V `)) . x = (G | (V `)) . x by A44; :: thesis:

end;

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

now :: thesis:

end;

then A50: rng ((Integral1 (M1,f)) | (V `)) c= REAL ;

now :: thesis:

end;

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

now :: thesis:

end;

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

now :: thesis:

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

end;

now :: thesis:

let x be Element of X2; :: thesis:
assume A79: x in dom (g | (V `)) ; :: thesis:
then A80: x in V ` by RELAT_1:57;
then A81: (g | (V `)) . x = (Integral1 (M1,f)) . x by A66, FUNCT_1:49;
ProjPMap2 (f,x) is_integrable_on M1 by A14, A79, RELAT_1:57;
then A82: ex A being Element of S1 st
( A = dom (ProjPMap2 (f,x)) & ProjPMap2 (f,x) is A -measurable ) by MESFUNC5:def 17;
( (Integral1 (M1,(max+ f))) . x = Integral (M1,(ProjPMap2 ((max+ f),x))) & (Integral1 (M1,(max- f))) . x = Integral (M1,(ProjPMap2 ((max- f),x))) ) by MESFUN12:def 7;
then ( (Integral1 (M1,(max+ f))) . x = Integral (M1,(max+ (ProjPMap2 (f,x)))) & (Integral1 (M1,(max- f))) . x = Integral (M1,(max- (ProjPMap2 (f,x)))) ) by MESFUN12:46;
then ((Integral1 (M1,(max+ f))) . x) - ((Integral1 (M1,(max- f))) . x) = Integral (M1,(ProjPMap2 (f,x))) by A82, MESFUN11:54
.= (Integral1 (M1,f)) . x by MESFUN12:def 7 ;
then (g | (V `)) . x = (((Integral1 (M1,(max+ f))) | (V `)) . x) - ((Integral1 (M1,(max- f))) . x) by A80, A81, FUNCT_1:49
.= ((g1 | (V `)) . x) - ((g2 | (V `)) . x) by A64, A65, A80, FUNCT_1:49 ;
hence (g | (V `)) . x = ((g1 | (V `)) - (g2 | (V `))) . x by A76, A79, MESFUNC1:def 4; :: thesis:

end;

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