theorem Th38: :: MEASUR13:38

for n being non zero Nat
for X being non-empty b₁ + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL st M is sigma_finite & f is_Sequentially_integrable_on M & f is_integrable_on Prod_Measure M holds
for k being non zero Nat st k < n + 1 holds
ex g being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL st
( g = (FSqIntg (M,f)) . ((n + 1) - k) & g is_integrable_on Prod_Measure (SubFin (M,(k + 1))) )