let X1, X2 be non empty set ; 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)) st M2 is sigma_finite holds
Y-vol (E,M2) = Integral2 (M2,(chi (E,[:X1,X2:])))
let S1 be 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)) st M2 is sigma_finite holds
Y-vol (E,M2) = Integral2 (M2,(chi (E,[:X1,X2:])))
let S2 be SigmaField of X2; for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds
Y-vol (E,M2) = Integral2 (M2,(chi (E,[:X1,X2:])))
let M2 be sigma_Measure of S2; for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds
Y-vol (E,M2) = Integral2 (M2,(chi (E,[:X1,X2:])))
let A be Element of sigma (measurable_rectangles (S1,S2)); ( M2 is sigma_finite implies Y-vol (A,M2) = Integral2 (M2,(chi (A,[:X1,X2:]))) )
assume a1:
M2 is sigma_finite
; Y-vol (A,M2) = Integral2 (M2,(chi (A,[:X1,X2:])))
now for x being Element of X1 holds (Y-vol (A,M2)) . x = (Integral2 (M2,(chi (A,[:X1,X2:])))) . xlet x be
Element of
X1;
(Y-vol (A,M2)) . x = (Integral2 (M2,(chi (A,[:X1,X2:])))) . xA1:
(Y-vol (A,M2)) . x = Integral (
M2,
(chi ((Measurable-X-section (A,x)),X2)))
by a1, Th62;
ProjPMap1 (
(chi (A,[:X1,X2:])),
x)
= chi (
(Measurable-X-section (A,x)),
X2)
by Th63;
hence
(Y-vol (A,M2)) . x = (Integral2 (M2,(chi (A,[:X1,X2:])))) . x
by A1, Def8;
verum end;
hence
Y-vol (A,M2) = Integral2 (M2,(chi (A,[:X1,X2:])))
by FUNCT_2:def 8; verum