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 x being Element of X1
for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds
( (Y-vol (E,M2)) . x = Integral (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral+ (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral' (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for x being Element of X1
for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds
( (Y-vol (E,M2)) . x = Integral (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral+ (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral' (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) )
let S2 be SigmaField of X2; :: thesis: for M2 being sigma_Measure of S2
for x being Element of X1
for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds
( (Y-vol (E,M2)) . x = Integral (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral+ (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral' (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) )
let M2 be sigma_Measure of S2; :: thesis: for x being Element of X1
for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds
( (Y-vol (E,M2)) . x = Integral (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral+ (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral' (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) )
let x be Element of X1; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds
( (Y-vol (E,M2)) . x = Integral (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral+ (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral' (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) )
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( M2 is sigma_finite implies ( (Y-vol (E,M2)) . x = Integral (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral+ (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral' (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) ) )
assume A1: M2 is sigma_finite ; :: thesis: ( (Y-vol (E,M2)) . x = Integral (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral+ (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral' (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) )
A2: ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((X-section (E,x)),X2) by Th48;
then ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((Measurable-X-section (E,x)),X2) by MEASUR11:def 6;
then A4: ProjPMap1 ((chi (E,[:X1,X2:])),x) is_simple_func_in S2 by Th12;
(Y-vol (E,M2)) . x = M2 . (Measurable-X-section (E,x)) by A1, MEASUR11:def 13;
then (Y-vol (E,M2)) . x = Integral (M2,(ProjMap1 ((chi (E,[:X1,X2:])),x))) by MEASUR11:72;
hence (Y-vol (E,M2)) . x = Integral (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) by Th27; :: thesis: ( (Y-vol (E,M2)) . x = integral+ (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral' (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) )
hence ( (Y-vol (E,M2)) . x = integral+ (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral' (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) ) by A2, A4, MESFUNC5:89; :: thesis: verum