theorem Th36:
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
f1 being
PartFunc of
[:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],
ExtREAL for
f2 being
PartFunc of
(CarProduct (SubFin (X,(n + 1)))),
ExtREAL st
M is
sigma_finite &
f = f1 &
f = f2 &
f is_integrable_on Prod_Measure M & ( for
x being
Element of
CarProduct (SubFin (X,n)) holds
(Integral2 ((ElmFin (M,(n + 1))),|.f1.|)) . x < +infty ) holds
Integral (
(Prod_Measure (SubFin (M,(n + 1)))),
f2)
= Integral (
(Prod_Measure (SubFin (M,n))),
(Integral2 ((ElmFin (M,(n + 1))),f1)))