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)) st M1 is sigma_finite holds
X-vol (E,M1) = Integral1 (M1,(chi (E,[:X1,X2:])))
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)) st M1 is sigma_finite holds
X-vol (E,M1) = Integral1 (M1,(chi (E,[:X1,X2:])))
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
X-vol (E,M1) = Integral1 (M1,(chi (E,[:X1,X2:])))
let M1 be sigma_Measure of S1; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
X-vol (E,M1) = Integral1 (M1,(chi (E,[:X1,X2:])))
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( M1 is sigma_finite implies X-vol (A,M1) = Integral1 (M1,(chi (A,[:X1,X2:]))) )
assume A1: M1 is sigma_finite ; :: thesis: X-vol (A,M1) = Integral1 (M1,(chi (A,[:X1,X2:])))

now :: thesis: for y being Element of X2 holds (X-vol (A,M1)) . y = (Integral1 (M1,(chi (A,[:X1,X2:])))) . y

let y be Element of X2; :: thesis: (X-vol (A,M1)) . y = (Integral1 (M1,(chi (A,[:X1,X2:])))) . y
A2: (X-vol (A,M1)) . y = Integral (M1,(chi ((Measurable-Y-section (A,y)),X1))) by A1, Th61;
ProjPMap2 ((chi (A,[:X1,X2:])),y) = chi ((Measurable-Y-section (A,y)),X1) by Th63;
hence (X-vol (A,M1)) . y = (Integral1 (M1,(chi (A,[:X1,X2:])))) . y by A2, Def7; :: thesis: verum

end;

hence X-vol (A,M1) = Integral1 (M1,(chi (A,[:X1,X2:]))) by FUNCT_2:def 8; :: thesis: verum