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 y being Element of X2
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
(X-vol (E,M1)) . y = Integral (M1,(chi ((Measurable-Y-section (E,y)),X1)))
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for y being Element of X2
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
(X-vol (E,M1)) . y = Integral (M1,(chi ((Measurable-Y-section (E,y)),X1)))
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for y being Element of X2
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
(X-vol (E,M1)) . y = Integral (M1,(chi ((Measurable-Y-section (E,y)),X1)))
let M1 be sigma_Measure of S1; :: thesis: for y being Element of X2
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
(X-vol (E,M1)) . y = Integral (M1,(chi ((Measurable-Y-section (E,y)),X1)))
let y be Element of X2; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
(X-vol (E,M1)) . y = Integral (M1,(chi ((Measurable-Y-section (E,y)),X1)))
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( M1 is sigma_finite implies (X-vol (A,M1)) . y = Integral (M1,(chi ((Measurable-Y-section (A,y)),X1))) )
assume M1 is sigma_finite ; :: thesis: (X-vol (A,M1)) . y = Integral (M1,(chi ((Measurable-Y-section (A,y)),X1)))
then (X-vol (A,M1)) . y = M1 . (Measurable-Y-section (A,y)) by MEASUR11:def 14;
hence (X-vol (A,M1)) . y = Integral (M1,(chi ((Measurable-Y-section (A,y)),X1))) by MESFUNC9:14; :: thesis: verum