theorem Th35:
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
fn1 being
PartFunc of
[:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],
ExtREAL st
M is
sigma_finite &
f = fn1 &
f is_integrable_on Prod_Measure M & ( for
x being
Element of
CarProduct (SubFin (X,n)) holds
(Integral2 ((ElmFin (M,(n + 1))),|.fn1.|)) . x < +infty ) holds
(
Integral (
(Prod_Measure M),
f)
= Integral (
(Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))),
fn1) & ( for
x being
Element of
CarProduct (SubFin (X,n)) holds
ProjPMap1 (
fn1,
x)
is_integrable_on ElmFin (
M,
(n + 1)) ) & ( for
U being
Element of
Prod_Field (SubFin (S,n)) holds
Integral2 (
(ElmFin (M,(n + 1))),
fn1) is
U -measurable ) &
Integral2 (
(ElmFin (M,(n + 1))),
fn1)
is_integrable_on Prod_Measure (SubFin (M,n)) &
Integral (
(Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))),
fn1)
= Integral (
(Prod_Measure (SubFin (M,n))),
(Integral2 ((ElmFin (M,(n + 1))),fn1))) &
Integral2 (
(ElmFin (M,(n + 1))),
fn1)
in L1_Functions (Prod_Measure (SubFin (M,n))) )