theorem Th32:
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 st
f is_integrable_on Prod_Measure M holds
ex
g being
PartFunc of
[:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],
ExtREAL st
(
f = g &
g is_integrable_on Prod_Measure (
(Prod_Measure (SubFin (M,n))),
(ElmFin (M,(n + 1)))) &
Integral (
(Prod_Measure M),
f)
= Integral (
(Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))),
g) )