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
g being
PartFunc of
[:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],
ExtREAL st
M is
sigma_finite &
f is_integrable_on Prod_Measure M &
f = g & ( for
y being
Element of
ElmFin (
X,
(n + 1)) holds
(Integral1 ((Prod_Measure (SubFin (M,n))),|.g.|)) . y < +infty ) holds
( ( for
y being
Element of
ElmFin (
X,
(n + 1)) holds
ProjPMap2 (
g,
y)
is_integrable_on Prod_Measure (SubFin (M,n)) ) & ( for
V being
Element of
ElmFin (
S,
(n + 1)) holds
Integral1 (
(Prod_Measure (SubFin (M,n))),
g) is
V -measurable ) &
Integral1 (
(Prod_Measure (SubFin (M,n))),
g)
is_integrable_on ElmFin (
M,
(n + 1)) &
Integral (
(Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))),
g)
= Integral (
(ElmFin (M,(n + 1))),
(Integral1 ((Prod_Measure (SubFin (M,n))),g))) &
Integral1 (
(Prod_Measure (SubFin (M,n))),
g)
in L1_Functions (ElmFin (M,(n + 1))) )