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:
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: for x being Element of X1 holds (Integral2 (M2,|.f.|)) . x < +infty ; :: thesis:
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
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.| by A5, MESFUNC1:def 10;

A7: now :: thesis:

let x be Element of X1; :: thesis:
X-section (A,x) = Measurable-X-section (A,x) by MEASUR11:def 6;
then A8: dom (ProjPMap1 (|.f.|,x)) = Measurable-X-section (A,x) by A6, MESFUN12:def 3;
A9: |.f.| is A -measurable by A5, MESFUNC2:27;
then A10: ProjPMap1 (|.f.|,x) is Measurable-X-section (A,x) -measurable by A6, MESFUN12:47;
A11: 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, A8, A9, A11, MESFUNC5:88, MESFUN12:47
.= (Integral2 (M2,|.f.|)) . x by MESFUN12:def 8 ;
then A12: integral+ (M2,(max+ (ProjPMap1 (|.f.|,x)))) < +infty by A4;
integral+ (M2,(max- (ProjPMap1 (|.f.|,x)))) = 0 by A8, A10, A11, MESFUN11:53;
then A13: ProjPMap1 (|.f.|,x) is_integrable_on M2 by A6, A8, A9, A12, MESFUNC5:def 17, MESFUN12:47;
A14: dom (ProjPMap1 (f,x)) = Measurable-X-section (A,x) by A8, A11, MESFUNC1:def 10;
ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable by A5, MESFUN12:47;
hence ProjPMap1 (f,x) is_integrable_on M2 by A11, A13, A14, MESFUNC5:100; :: thesis:

end;

hence for x being Element of X1 holds ProjPMap1 (f,x) is_integrable_on M2 ; :: thesis:
set G1 = Integral2 (M2,(max+ f));
set G2 = Integral2 (M2,(max- f));
set G = (Integral2 (M2,(max+ f))) - (Integral2 (M2,(max- f)));
A15: ( dom (Integral2 (M2,(max+ f))) = X1 & dom (Integral2 (M2,(max- f))) = X1 & dom (Integral2 (M2,f)) = X1 & dom (Integral2 (M2,|.f.|)) = X1 ) by FUNCT_2:def 1;

A16: now :: thesis:

let x be object ; :: thesis:

per cases ;

suppose x in dom (Integral2 (M2,(max+ f))) ; :: thesis:

then reconsider x1 = x as Element of X1 ;
(Integral2 (M2,(max+ f))) . x = Integral (M2,(ProjPMap1 ((max+ f),x1))) by MESFUN12:def 8;
then A17: (Integral2 (M2,(max+ f))) . x = Integral (M2,(max+ (ProjPMap1 (f,x1)))) by MESFUN12:45;
A18: ProjPMap1 (f,x1) is_integrable_on M2 by A7;
then consider B being Element of S2 such that
A19: ( B = dom (ProjPMap1 (f,x1)) & ProjPMap1 (f,x1) is B -measurable ) by MESFUNC5:def 17;
A20: ( B = dom (max+ (ProjPMap1 (f,x1))) & max+ (ProjPMap1 (f,x1)) is B -measurable ) by A19, MESFUNC2:def 2, MESFUN11:10;
integral+ (M2,(max+ (ProjPMap1 (f,x1)))) < +infty by A18, MESFUNC5:def 17;
hence (Integral2 (M2,(max+ f))) . x < +infty by A17, A20, MESFUNC5:88, MESFUN11:5; :: thesis:

end;

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

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

end;

now :: thesis:

let x be object ; :: thesis:

per cases ;

suppose x in dom (Integral2 (M2,(max+ f))) ; :: thesis:

then reconsider x1 = x as Element of X1 ;
(Integral2 (M2,(max+ f))) . x = Integral (M2,(ProjPMap1 ((max+ f),x1))) by MESFUN12:def 8;
then A21: (Integral2 (M2,(max+ f))) . x = Integral (M2,(max+ (ProjPMap1 (f,x1)))) by MESFUN12:45;
ProjPMap1 (f,x1) is_integrable_on M2 by A7;
then consider B being Element of S2 such that
A22: ( 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 A22, MESFUNC2:def 2, MESFUN11:10;
hence (Integral2 (M2,(max+ f))) . x > -infty by A21, MESFUNC5:90, MESFUN11:5; :: thesis:

end;

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

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

end;

then A23: ( Integral2 (M2,(max+ f)) is without-infty & Integral2 (M2,(max+ f)) is without+infty ) by A16, MESFUNC5:def 5, MESFUNC5:def 6;
then A24: dom ((Integral2 (M2,(max+ f))) - (Integral2 (M2,(max- f)))) = (dom (Integral2 (M2,(max+ f)))) /\ (dom (Integral2 (M2,(max- f)))) by MESFUN11:23;
TT: ( Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral2 (M2,(max- f)) is_integrable_on M1 ) by A1, A2, A3, Th20;
then A25: ex A1 being Element of S1 st
( A1 = dom (Integral2 (M2,(max+ f))) & Integral2 (M2,(max+ f)) is A1 -measurable ) by MESFUNC5:def 17;
A26: ex A2 being Element of S1 st
( A2 = dom (Integral2 (M2,(max- f))) & Integral2 (M2,(max- f)) is A2 -measurable ) by TT, MESFUNC5:def 17;

now :: thesis:

let x be object ; :: thesis:

per cases ;

suppose x in dom (Integral2 (M2,(max- f))) ; :: thesis:

then reconsider x1 = x as Element of X1 ;
(Integral2 (M2,(max- f))) . x = Integral (M2,(ProjPMap1 ((max- f),x1))) by MESFUN12:def 8;
then A27: (Integral2 (M2,(max- f))) . x = Integral (M2,(max- (ProjPMap1 (f,x1)))) by MESFUN12:45;
ProjPMap1 (f,x1) is_integrable_on M2 by A7;
then consider B being Element of S2 such that
A28: ( 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 A28, MESFUNC2:def 3, MESFUN11:10;
hence (Integral2 (M2,(max- f))) . x > -infty by A27, MESFUNC5:90, MESFUN11:5; :: thesis:

end;

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

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

end;

then Integral2 (M2,(max- f)) is without-infty by MESFUNC5:def 5;
then A29: (Integral2 (M2,(max+ f))) - (Integral2 (M2,(max- f))) is XX1 -measurable by A15, A23, A24, A25, A26, MEASUR11:66;

now :: thesis:

let x be Element of X1; :: thesis:
assume x in dom (Integral2 (M2,f)) ; :: thesis:
A30: (Integral2 (M2,f)) . x = Integral (M2,(ProjPMap1 (f,x))) by MESFUN12:def 8;
ProjPMap1 (f,x) is_integrable_on M2 by A7;
then B30: 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))) - (Integral2 (M2,(max- f)))) . x = ((Integral2 (M2,(max+ f))) . x) - ((Integral2 (M2,(max- f))) . x) by A15, A24, MESFUNC1:def 4
.= (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 ;
hence ((Integral2 (M2,(max+ f))) - (Integral2 (M2,(max- f)))) . x = (Integral2 (M2,f)) . x by A30, B30, MESFUN11:54; :: thesis:

end;

then A31: Integral2 (M2,f) = (Integral2 (M2,(max+ f))) - (Integral2 (M2,(max- f))) by A15, A24, PARTFUN1:5;
hence for U being Element of S1 holds Integral2 (M2,f) is U -measurable by A29, MESFUNC1:30; :: thesis:
A32: ( X1 = dom (max+ (Integral2 (M2,f))) & X1 = dom (max- (Integral2 (M2,f))) ) by A15, MESFUNC2:def 2, MESFUNC2:def 3;
A33: ( max+ (Integral2 (M2,f)) is XX1 -measurable & max- (Integral2 (M2,f)) is XX1 -measurable ) by A15, A29, A31, MESFUNC2:25, MESFUNC2:26;
A34: Integral2 (M2,|.f.|) is_integrable_on M1 by A1, A2, A3, Th20;

now :: thesis:

end;

then A37: max+ (Integral2 (M2,f)) is_integrable_on M1 by A15, A32, A33, A34, MESFUNC5:102;

now :: thesis:

end;

then max- (Integral2 (M2,f)) is_integrable_on M1 by A15, A32, A33, A34, MESFUNC5:102;
then (max+ (Integral2 (M2,f))) - (max- (Integral2 (M2,f))) is_integrable_on M1 by A37, MESFUN10:12;
hence A40: Integral2 (M2,f) is_integrable_on M1 by MESFUNC2:23; :: thesis:
A41: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;
A42: ( dom (max+ f) = A & dom (max- f) = A ) by A5, MESFUNC2:def 2, MESFUNC2:def 3;
A43: ( max+ f is A -measurable & max- f is A -measurable ) by A5, MESFUNC2:25, MESFUNC2:26;
then A44: Integral ((Prod_Measure (M1,M2)),(max- f)) = Integral (M1,(Integral2 (M2,(max- f)))) by A1, A2, A41, A42, MESFUN12:84;
Integral ((Prod_Measure (M1,M2)),f) = (Integral ((Prod_Measure (M1,M2)),(max+ f))) - (Integral ((Prod_Measure (M1,M2)),(max- f))) by A5, MESFUN11:54
.= (Integral (M1,((Integral2 (M2,(max+ f))) | XX1))) - (Integral (M1,((Integral2 (M2,(max- f))) | XX1))) by A1, A2, A41, A42, A43, A44, MESFUN12:84 ;
hence Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) by A15, A24, A31, TT, Th21; :: thesis:

now :: thesis:

let y be set ; :: thesis:
assume y in rng (Integral2 (M2,f)) ; :: thesis:
then consider x being Element of X1 such that
A45: ( x in dom (Integral2 (M2,f)) & y = (Integral2 (M2,f)) . x ) by PARTFUN1:3;
(Integral2 (M2,f)) . x = Integral (M2,(ProjPMap1 (f,x))) by MESFUN12:def 8;
then |.((Integral2 (M2,f)) . x).| <= Integral (M2,|.(ProjPMap1 (f,x)).|) by A7, MESFUNC5:101;
then |.((Integral2 (M2,f)) . x).| <= Integral (M2,(ProjPMap1 (|.f.|,x))) by Th27;
then |.((Integral2 (M2,f)) . x).| <= (Integral2 (M2,|.f.|)) . x by MESFUN12:def 8;
then |.((Integral2 (M2,f)) . x).| < +infty by A4, XXREAL_0:2;
hence y in REAL by A45, EXTREAL1:41; :: thesis:

end;

then rng (Integral2 (M2,f)) c= REAL ;
then reconsider F = Integral2 (M2,f) as PartFunc of X1,REAL by RELSET_1:6;
reconsider ND = {} as Element of S1 by MEASURE1:7;
A46: M1 . ND = 0 by VALUED_0:def 19;
ND ` = X1 \ {} by SUBSET_1:def 4
.= X1 ;
then A47: dom F = ND ` by FUNCT_2:def 1;
R_EAL F is_integrable_on M1 by A40, 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 A46, A47;
hence Integral2 (M2,f) in L1_Functions M1 by LPSPACE1:def 8; :: thesis: