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,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral+ (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral' (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) )
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,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral+ (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral' (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) )
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,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral+ (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral' (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) )
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,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral+ (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral' (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) )
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,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral+ (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral' (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) )
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( M1 is sigma_finite implies ( (X-vol (E,M1)) . y = Integral (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral+ (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral' (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) ) )
assume A1: M1 is sigma_finite ; :: thesis: ( (X-vol (E,M1)) . y = Integral (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral+ (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral' (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) )
A2: ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Y-section (E,y)),X1) by Th48;
then ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Measurable-Y-section (E,y)),X1) by MEASUR11:def 7;
then A4: ProjPMap2 ((chi (E,[:X1,X2:])),y) is_simple_func_in S1 by Th12;
(X-vol (E,M1)) . y = M1 . (Measurable-Y-section (E,y)) by A1, MEASUR11:def 14;
then (X-vol (E,M1)) . y = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) by MEASUR11:72;
hence (X-vol (E,M1)) . y = Integral (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) by Th27; :: thesis: ( (X-vol (E,M1)) . y = integral+ (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral' (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) )
hence ( (X-vol (E,M1)) . y = integral+ (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral' (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) ) by A2, A4, MESFUNC5:89; :: thesis: verum