theorem
for
X1,
X2 being non
empty set for
S1 being
SigmaField of
X1 for
S2 being
SigmaField of
X2 for
M1 being
sigma_Measure of
S1 for
M2 being
sigma_Measure of
S2 for
f being
PartFunc of
[:X1,X2:],
ExtREAL for
SX2 being
Element of
S2 st
M1 is
sigma_finite &
M2 is
sigma_finite &
f is_integrable_on Prod_Measure (
M1,
M2) &
X2 = SX2 holds
ex
V being
Element of
S2 st
(
M2 . V = 0 & ( for
y being
Element of
X2 st
y in V ` holds
ProjPMap2 (
f,
y)
is_integrable_on M1 ) &
(Integral1 (M1,|.f.|)) | (V `) is
PartFunc of
X2,
REAL &
Integral1 (
M1,
f) is
SX2 \ V -measurable &
(Integral1 (M1,f)) | (V `) is_integrable_on M2 &
(Integral1 (M1,f)) | (V `) in L1_Functions M2 & ex
g being
Function of
X2,
ExtREAL st
(
g is_integrable_on M2 &
g | (V `) = (Integral1 (M1,f)) | (V `) &
Integral (
(Prod_Measure (M1,M2)),
f)
= Integral (
M2,
g) ) )