let X1, X2 be non empty set ; :: thesis: 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
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is E1 -measurable holds
( Integral1 (M1,f) is nonnegative & Integral1 (M1,(f | E2)) is nonnegative & Integral2 (M2,f) is nonnegative & Integral2 (M2,(f | E2)) is nonnegative )
let S1 be SigmaField of X1; :: thesis: 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
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is E1 -measurable holds
( Integral1 (M1,f) is nonnegative & Integral1 (M1,(f | E2)) is nonnegative & Integral2 (M2,f) is nonnegative & Integral2 (M2,(f | E2)) is nonnegative )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is E1 -measurable holds
( Integral1 (M1,f) is nonnegative & Integral1 (M1,(f | E2)) is nonnegative & Integral2 (M2,f) is nonnegative & Integral2 (M2,(f | E2)) is nonnegative )
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is E1 -measurable holds
( Integral1 (M1,f) is nonnegative & Integral1 (M1,(f | E2)) is nonnegative & Integral2 (M2,f) is nonnegative & Integral2 (M2,(f | E2)) is nonnegative )
let M2 be sigma_Measure of S2; :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is E1 -measurable holds
( Integral1 (M1,f) is nonnegative & Integral1 (M1,(f | E2)) is nonnegative & Integral2 (M2,f) is nonnegative & Integral2 (M2,(f | E2)) is nonnegative )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is E1 -measurable holds
( Integral1 (M1,f) is nonnegative & Integral1 (M1,(f | E2)) is nonnegative & Integral2 (M2,f) is nonnegative & Integral2 (M2,(f | E2)) is nonnegative )
let A, B be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( A = dom f & f is nonnegative & f is A -measurable implies ( Integral1 (M1,f) is nonnegative & Integral1 (M1,(f | B)) is nonnegative & Integral2 (M2,f) is nonnegative & Integral2 (M2,(f | B)) is nonnegative ) )
assume that
A1: A = dom f and
A2: f is nonnegative and
A3: f is A -measurable ; :: thesis: ( Integral1 (M1,f) is nonnegative & Integral1 (M1,(f | B)) is nonnegative & Integral2 (M2,f) is nonnegative & Integral2 (M2,(f | B)) is nonnegative )
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: for y being object st y in dom (Integral1 (M1,f)) holds
(Integral1 (M1,f)) . y >= 0

let y be object ; :: thesis: ( y in dom (Integral1 (M1,f)) implies (Integral1 (M1,f)) . y >= 0 )
assume y in dom (Integral1 (M1,f)) ; :: thesis: (Integral1 (M1,f)) . y >= 0
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: verum

end;

hence Integral1 (M1,f) is nonnegative by SUPINF_2:52; :: thesis: ( Integral1 (M1,(f | B)) is nonnegative & Integral2 (M2,f) is nonnegative & Integral2 (M2,(f | B)) is nonnegative )

now :: thesis: for y being object st y in dom (Integral1 (M1,(f | B))) holds
(Integral1 (M1,(f | B))) . y >= 0

let y be object ; :: thesis: ( y in dom (Integral1 (M1,(f | B))) implies (Integral1 (M1,(f | B))) . y >= 0 )
assume y in dom (Integral1 (M1,(f | B))) ; :: thesis: (Integral1 (M1,(f | B))) . y >= 0
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: verum

end;

hence Integral1 (M1,(f | B)) is nonnegative by SUPINF_2:52; :: thesis: ( Integral2 (M2,f) is nonnegative & Integral2 (M2,(f | B)) is nonnegative )

now :: thesis: for x being object st x in dom (Integral2 (M2,f)) holds
(Integral2 (M2,f)) . x >= 0

let x be object ; :: thesis: ( x in dom (Integral2 (M2,f)) implies (Integral2 (M2,f)) . x >= 0 )
assume x in dom (Integral2 (M2,f)) ; :: thesis: (Integral2 (M2,f)) . x >= 0
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: verum

end;

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

now :: thesis: for x being object st x in dom (Integral2 (M2,(f | B))) holds
(Integral2 (M2,(f | B))) . x >= 0

let x be object ; :: thesis: ( x in dom (Integral2 (M2,(f | B))) implies (Integral2 (M2,(f | B))) . x >= 0 )
assume x in dom (Integral2 (M2,(f | B))) ; :: thesis: (Integral2 (M2,(f | B))) . x >= 0
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: verum

end;

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