theorem Th56:
for
X1,
X2 being non
empty set 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)) for
r being
Real st
M2 is
sigma_finite holds
(
(r (#) (Y-vol (E,M2))) . x = Integral (
M2,
(ProjPMap1 ((chi (r,E,[:X1,X2:])),x))) & (
r >= 0 implies
(r (#) (Y-vol (E,M2))) . x = integral+ (
M2,
(ProjPMap1 ((chi (r,E,[:X1,X2:])),x))) ) )