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
SX1 being
Element of
S1 st
M1 is
sigma_finite &
M2 is
sigma_finite &
f is_integrable_on Prod_Measure (
M1,
M2) &
X1 = SX1 holds
ex
U being
Element of
S1 st
(
M1 . U = 0 & ( for
x being
Element of
X1 st
x in U ` holds
ProjPMap1 (
f,
x)
is_integrable_on M2 ) &
(Integral2 (M2,|.f.|)) | (U `) is
PartFunc of
X1,
REAL &
Integral2 (
M2,
f) is
SX1 \ U -measurable &
(Integral2 (M2,f)) | (U `) is_integrable_on M1 &
(Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex
g being
Function of
X1,
ExtREAL st
(
g is_integrable_on M1 &
g | (U `) = (Integral2 (M2,f)) | (U `) &
Integral (
(Prod_Measure (M1,M2)),
f)
= Integral (
M1,
g) ) )