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 A, B be Element of sigma (measurable_rectangles (S1,S2)); :: thesis:
assume that
A1: A = dom f and
A2: f is nonnegative and
A3: f is A -measurable ; :: thesis:
A4: f | B is nonnegative by A2, MESFUNC5:15;
A5: dom (f | B) = A /\ B by A1, RELAT_1:61;
A6: f is A /\ B -measurable by A3, XBOOLE_1:17, MESFUNC1:30;
A7: (dom f) /\ (A /\ B) = A /\ B by A1, XBOOLE_1:17, XBOOLE_1:28;
f | (A /\ B) = (f | A) /\ (f | B) by RELAT_1:79;
then f | (A /\ B) = f | B by A1, RELAT_1:59, XBOOLE_1:28;
then A8: f | B is A /\ B -measurable by A6, A7, MESFUNC5:42;

now :: thesis:

let y be object ; :: thesis:
assume y in dom (Integral1 (M1,f)) ; :: thesis:
then reconsider y1 = y as Element of X2 ;
A9: ProjPMap2 (f,y1) is Measurable-Y-section (A,y1) -measurable by A1, A3, Th47;
dom (ProjPMap2 (f,y1)) = Y-section (A,y1) by A1, Def4;
then A10: dom (ProjPMap2 (f,y1)) = Measurable-Y-section (A,y1) by MEASUR11:def 7;
then integral+ (M1,(ProjPMap2 (f,y1))) >= 0 by A2, A9, Th32, MESFUNC5:79;
then Integral (M1,(ProjPMap2 (f,y1))) >= 0 by A2, A9, A10, Th32, MESFUNC5:88;
hence (Integral1 (M1,f)) . y >= 0 by Def7; :: thesis:

end;

hence Integral1 (M1,f) is V112() by SUPINF_2:52; :: thesis:

now :: thesis:

let y be object ; :: thesis:
assume y in dom (Integral1 (M1,(f | B))) ; :: thesis:
then reconsider y1 = y as Element of X2 ;
A11: ProjPMap2 ((f | B),y1) is Measurable-Y-section ((A /\ B),y1) -measurable by A5, A8, Th47;
dom (ProjPMap2 ((f | B),y1)) = Y-section ((A /\ B),y1) by A5, Def4;
then A12: dom (ProjPMap2 ((f | B),y1)) = Measurable-Y-section ((A /\ B),y1) by MEASUR11:def 7;
then integral+ (M1,(ProjPMap2 ((f | B),y1))) >= 0 by A4, A11, Th32, MESFUNC5:79;
then Integral (M1,(ProjPMap2 ((f | B),y1))) >= 0 by A4, A11, A12, Th32, MESFUNC5:88;
hence (Integral1 (M1,(f | B))) . y >= 0 by Def7; :: thesis:

end;

hence Integral1 (M1,(f | B)) is V112() by SUPINF_2:52; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom (Integral2 (M2,f)) ; :: thesis:
then reconsider x1 = x as Element of X1 ;
A13: ProjPMap1 (f,x1) is Measurable-X-section (A,x1) -measurable by A1, A3, Th47;
dom (ProjPMap1 (f,x1)) = X-section (A,x1) by A1, Def3;
then A14: dom (ProjPMap1 (f,x1)) = Measurable-X-section (A,x1) by MEASUR11:def 6;
then integral+ (M2,(ProjPMap1 (f,x1))) >= 0 by A2, A13, Th32, MESFUNC5:79;
then Integral (M2,(ProjPMap1 (f,x1))) >= 0 by A2, A13, A14, Th32, MESFUNC5:88;
hence (Integral2 (M2,f)) . x >= 0 by Def8; :: thesis:

end;

hence Integral2 (M2,f) is V112() by SUPINF_2:52; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom (Integral2 (M2,(f | B))) ; :: thesis:
then reconsider x1 = x as Element of X1 ;
A15: ProjPMap1 ((f | B),x1) is Measurable-X-section ((A /\ B),x1) -measurable by A5, A8, Th47;
dom (ProjPMap1 ((f | B),x1)) = X-section ((A /\ B),x1) by A5, Def3;
then A16: dom (ProjPMap1 ((f | B),x1)) = Measurable-X-section ((A /\ B),x1) by MEASUR11:def 6;
then integral+ (M2,(ProjPMap1 ((f | B),x1))) >= 0 by A4, A15, Th32, MESFUNC5:79;
then Integral (M2,(ProjPMap1 ((f | B),x1))) >= 0 by A4, A15, A16, Th32, MESFUNC5:88;
hence (Integral2 (M2,(f | B))) . x >= 0 by Def8; :: thesis:

end;

hence Integral2 (M2,(f | B)) is V112() by SUPINF_2:52; :: thesis: