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 g be PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL; :: thesis:
assume that
A1: M is sigma_finite and
A2: f is_integrable_on Prod_Measure M and
A3: f = g and
A4: for y being Element of ElmFin (X,(n + 1)) holds (Integral1 ((Prod_Measure (SubFin (M,n))),|.g.|)) . y < +infty ; :: thesis:
A5: ex g0 being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st
( f = g0 & g0 is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) & Integral ((Prod_Measure M),f) = Integral ((Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))),g0) ) by A2, Th32;
A6: n < n + 1 by NAT_1:13;
then A7: SubFin (X,n) = X | n by Def5;
A8: ElmFin (X,(n + 1)) = X . (n + 1) by Def1;
A9: SubFin (S,n) = S | n by A6, Def6;
A10: ElmFin (S,(n + 1)) = S . (n + 1) by Def7;
A11: SubFin (M,n) = M | n by A6, Def9;
A12: ElmFin (M,(n + 1)) = M . (n + 1) by Def10;
for j being Nat st j in Seg n holds
ex Xj being non empty set ex Sj being SigmaField of Xj ex mj being sigma_Measure of Sj st
( Xj = (SubFin (X,n)) . j & Sj = (SubFin (S,n)) . j & mj = (SubFin (M,n)) . j & mj is sigma_finite )

proof

let j be Nat; :: thesis:
assume A13: j in Seg n ; :: thesis:
Seg n c= Seg (n + 1) by FINSEQ_3:18;
then consider Xj being non empty set , Sj being SigmaField of Xj, mj being sigma_Measure of Sj such that
A14: ( Xj = X . j & Sj = S . j & mj = M . j & mj is sigma_finite ) by A1, A13;
take Xj ; :: thesis:
take Sj ; :: thesis:
take mj ; :: thesis:
thus Xj = (SubFin (X,n)) . j by A7, A13, A14, FUNCT_1:49; :: thesis:
thus Sj = (SubFin (S,n)) . j by A9, A13, A14, FUNCT_1:49; :: thesis:
thus mj = (SubFin (M,n)) . j by A11, A13, A14, FUNCT_1:49; :: thesis:
thus mj is sigma_finite by A14; :: thesis:

end;

then SubFin (M,n) is sigma_finite ;
then A15: Prod_Measure (SubFin (M,n)) is sigma_finite by Th29;
ex Xi being non empty set ex Fi being SigmaField of Xi ex mi being sigma_Measure of Fi st
( Xi = X . (n + 1) & Fi = S . (n + 1) & mi = M . (n + 1) & mi is sigma_finite ) by A1, FINSEQ_1:4;
hence ( ( 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))) ) by A3, A4, A5, A15, A8, A10, A12, MESFUN13:33; :: thesis: