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 E being Element of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 holds
( ( M1 . (Measurable-Y-section (E,y)) <> 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = +infty ) & ( M1 . (Measurable-Y-section (E,y)) = 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = 0 ) )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for E being Element of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 holds
( ( M1 . (Measurable-Y-section (E,y)) <> 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = +infty ) & ( M1 . (Measurable-Y-section (E,y)) = 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = 0 ) )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for E being Element of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 holds
( ( M1 . (Measurable-Y-section (E,y)) <> 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = +infty ) & ( M1 . (Measurable-Y-section (E,y)) = 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = 0 ) )
let M1 be sigma_Measure of S1; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 holds
( ( M1 . (Measurable-Y-section (E,y)) <> 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = +infty ) & ( M1 . (Measurable-Y-section (E,y)) = 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = 0 ) )
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for y being Element of X2 holds
( ( M1 . (Measurable-Y-section (E,y)) <> 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = +infty ) & ( M1 . (Measurable-Y-section (E,y)) = 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = 0 ) )
let y be Element of X2; :: thesis: ( ( M1 . (Measurable-Y-section (E,y)) <> 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = +infty ) & ( M1 . (Measurable-Y-section (E,y)) = 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = 0 ) )
ProjPMap2 ((Xchi (E,[:X1,X2:])),y) = Xchi ((Y-section (E,y)),X1) by MESFUN12:35;
then A1: (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = Integral (M1,(Xchi ((Y-section (E,y)),X1))) by MESFUN12:def 7;
A2: Measurable-Y-section (E,y) = Y-section (E,y) by MEASUR11:def 7;
hence ( M1 . (Measurable-Y-section (E,y)) <> 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = +infty ) by A1, MEASUR10:33; :: thesis: ( M1 . (Measurable-Y-section (E,y)) = 0 implies (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = 0 )
assume M1 . (Measurable-Y-section (E,y)) = 0 ; :: thesis: (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = 0
hence (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y = 0 by A1, A2, MEASUR10:33; :: thesis: verum