theorem :: MEASUR13:40

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 holds
ex Fk1 being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL ex Gk1 being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL ex Fk being Function of (CarProduct (SubFin (X,k))),ExtREAL st
( Gk1 = Fk1 & Gk1 = (FSqIntg (M,f)) . ((n + 1) - k) & Fk = (FSqIntg (M,f)) . ((n + 1) - (k - 1)) & Fk = Integral2 ((ElmFin (M,(k + 1))),Fk1) & Gk1 is_integrable_on Prod_Measure (SubFin (M,(k + 1))) & Integral ((Prod_Measure (SubFin (M,(k + 1)))),Gk1) = Integral ((Prod_Measure ((Prod_Measure (SubFin (M,k))),(ElmFin (M,(k + 1))))),Fk1) & ( for x being Element of CarProduct (SubFin (X,k)) holds ProjPMap1 (Fk1,x) is_integrable_on ElmFin (M,(k + 1)) ) & ( for U being Element of Prod_Field (SubFin (S,k)) holds Fk is U -measurable ) & Fk is_integrable_on Prod_Measure (SubFin (M,k)) & Integral ((Prod_Measure ((Prod_Measure (SubFin (M,k))),(ElmFin (M,(k + 1))))),Fk1) = Integral ((Prod_Measure (SubFin (M,k))),Fk) & Fk in L1_Functions (Prod_Measure (SubFin (M,k))) & Integral ((Prod_Measure (SubFin (M,(k + 1)))),Gk1) = Integral ((Prod_Measure (SubFin (M,k))),Fk) )