let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 holds
( ( M2 . (Measurable-X-section (E,x)) <> 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = +infty ) & ( M2 . (Measurable-X-section (E,x)) = 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = 0 ) )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 holds
( ( M2 . (Measurable-X-section (E,x)) <> 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = +infty ) & ( M2 . (Measurable-X-section (E,x)) = 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = 0 ) )
let S2 be SigmaField of X2; :: thesis: for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 holds
( ( M2 . (Measurable-X-section (E,x)) <> 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = +infty ) & ( M2 . (Measurable-X-section (E,x)) = 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = 0 ) )
let M2 be sigma_Measure of S2; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 holds
( ( M2 . (Measurable-X-section (E,x)) <> 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = +infty ) & ( M2 . (Measurable-X-section (E,x)) = 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = 0 ) )
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for x being Element of X1 holds
( ( M2 . (Measurable-X-section (E,x)) <> 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = +infty ) & ( M2 . (Measurable-X-section (E,x)) = 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = 0 ) )
let x be Element of X1; :: thesis: ( ( M2 . (Measurable-X-section (E,x)) <> 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = +infty ) & ( M2 . (Measurable-X-section (E,x)) = 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = 0 ) )
ProjPMap1 ((Xchi (E,[:X1,X2:])),x) = Xchi ((X-section (E,x)),X2) by MESFUN12:35;
then A1: (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = Integral (M2,(Xchi ((X-section (E,x)),X2))) by MESFUN12:def 8;
A2: Measurable-X-section (E,x) = X-section (E,x) by MEASUR11:def 6;
hence ( M2 . (Measurable-X-section (E,x)) <> 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = +infty ) by A1, MEASUR10:33; :: thesis: ( M2 . (Measurable-X-section (E,x)) = 0 implies (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = 0 )
assume M2 . (Measurable-X-section (E,x)) = 0 ; :: thesis: (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = 0
hence (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x = 0 by A1, A2, MEASUR10:33; :: thesis: verum