let n be non zero Nat; :: thesis:
let X be non-empty n + 1 -element FinSequence; :: thesis:
let S be sigmaFieldFamily of X; :: thesis:
let M be sigmaMeasureFamily of S; :: thesis:
let f be PartFunc of (CarProduct X),ExtREAL; :: thesis:
let fn1 be PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL; :: thesis:
assume that
A1: M is sigma_finite and
A2: f = fn1 and
A3: f is_integrable_on Prod_Measure M and
A4: for x being Element of CarProduct (SubFin (X,n)) holds (Integral2 ((ElmFin (M,(n + 1))),|.fn1.|)) . x < +infty ; :: thesis:
A5: CarProduct X = [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):] by Th6;
A6: Prod_Measure M = Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) by Th28;
A7: n < n + 1 by NAT_1:13;
then A8: Prod_Measure (SubFin (M,n)) is sigma_finite by A1, Th29, Th30;
A9: ElmFin (M,(n + 1)) is sigma_finite by Th31, A1;
A10: len X = n + 1 by CARD_1:def 7;
SubFin (X,(n + 1)) = X | (n + 1) by Def5;
then A11: X = SubFin (X,(n + 1)) by A10, FINSEQ_1:58;
A12: len S = n + 1 by CARD_1:def 7;
SubFin (S,(n + 1)) = S | (n + 1) by Def6;
then S = SubFin (S,(n + 1)) by A12, FINSEQ_1:58;
then Prod_Field S = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1))))) by A7, A11, Th21;
hence ( 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))) ) by A4, A2, A3, A5, A6, A8, A9, MESFUN13:32; :: thesis: