theorem
for
n being non
zero Nat for
X being
non-empty b1 + 1
-element FinSequence for
S being
sigmaFieldFamily of
X for
M being
sigmaMeasureFamily of
S for
f being
PartFunc of
(CarProduct X),
ExtREAL for
E being
Element of
Prod_Field S for
g being
PartFunc of
[:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],
ExtREAL st
M is
sigma_finite &
E = dom f &
f is
E -measurable &
f = g holds
(
g is_integrable_on Prod_Measure (
(Prod_Measure (SubFin (M,n))),
(ElmFin (M,(n + 1)))) iff
Integral (
(Prod_Measure (SubFin (M,n))),
(Integral2 ((ElmFin (M,(n + 1))),|.g.|)))
< +infty )