defpred S₁[ Nat, set , set ] means ( ex i being non zero Nat st
( i = $1 & $2 is sigma_Measure of (Prod_Field (SubFin (S,i))) ) implies ex i being non zero Nat ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( i = $1 & $2 = Mi & $3 = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) );
A1: for n being Nat st 1 <= n & n < m holds
for x being set ex y being set st S₁[n,x,y]

let n be Nat; :: thesis:
assume ( 1 <= n & n < m ) ; :: thesis:
let x be set ; :: thesis:

assume ex k being non zero Nat st
( k = n & x is sigma_Measure of (Prod_Field (SubFin (S,k))) ) ; :: thesis:
then consider k being non zero Nat such that
A2: ( k = n & x is sigma_Measure of (Prod_Field (SubFin (S,k))) ) ;
reconsider Mn = x as sigma_Measure of (Prod_Field (SubFin (S,k))) by A2;
reconsider y = product_sigma_Measure (Mn,(ElmFin (M,(n + 1)))) as set ;
take y = y; :: thesis:
thus S₁[n,x,y] by A2; :: thesis:

end;

hence ex y being set st S₁[n,x,y] ; :: thesis:

end;

consider PM being FinSequence such that
A3: ( len PM = m & ( PM . 1 = M . 1 or m = 0 ) & ( for n being Nat st 1 <= n & n < m holds
S₁[n,PM . n,PM . (n + 1)] ) ) from RECDEF_1:sch 3(A1);
reconsider PM = PM as m -element FinSequence by A3, CARD_1:def 7;
defpred S₂[ Nat] means ( 1 <= $1 & $1 <= m implies ex k being non zero Nat st
( k = $1 & PM . $1 is sigma_Measure of (Prod_Field (SubFin (S,k))) ) );
A4: S₂[ 0 ] ;
A5: for n being Nat st S₂[n] holds
S₂[n + 1]

let n be Nat; :: thesis:
assume A6: S₂[n] ; :: thesis:
assume A7: ( 1 <= n + 1 & n + 1 <= m ) ; :: thesis:

suppose A8: n = 0 ; :: thesis:

reconsider k = 1 as non zero Nat ;
take k ; :: thesis:
thus k = n + 1 by A8; :: thesis:
1 <= m by NAT_1:14;
then 1 in Seg m ;
then A9: ex Sk being SigmaField of (X . k) st
( Sk = S . k & M . k is sigma_Measure of Sk ) by Def8;
A10: SubFin (X,k) = X | 1 by Def5, NAT_1:14;
A11: 1 in Seg 1 ;
then (SubFin (X,k)) . 1 = X . 1 by A10, FUNCT_1:49;
then A12: CarProduct (SubFin (X,k)) = X . 1 by Def3;
SubFin (S,k) = S | 1 by Def6, NAT_1:14;
then A13: (SubFin (S,k)) . 1 = S . 1 by A11, FUNCT_1:49;
Prod_Field (SubFin (S,k)) = (SubFin (S,k)) . 1 by Def11;
hence PM . (n + 1) is sigma_Measure of (Prod_Field (SubFin (S,k))) by A9, A3, A8, A12, A13; :: thesis:

end;

suppose n <> 0 ; :: thesis:

then A14: ( 1 <= n & n < m ) by A7, NAT_1:13, NAT_1:14;
then consider k0 being non zero Nat, PMk0 being sigma_Measure of (Prod_Field (SubFin (S,k0))) such that
A15: ( k0 = n & PM . n = PMk0 & PM . (n + 1) = product_sigma_Measure (PMk0,(ElmFin (M,(k0 + 1)))) ) by A3, A6;
A16: PM . (k0 + 1) is sigma_Measure of (sigma (measurable_rectangles ((Prod_Field (SubFin (S,k0))),(ElmFin (S,(k0 + 1)))))) by A15, MEASUR11:8;
A17: [:(CarProduct (SubFin (X,k0))),(ElmFin (X,(k0 + 1))):] = CarProduct (SubFin (X,(k0 + 1))) by A14, A15, Th9;
Prod_Field (SubFin (S,(k0 + 1))) = sigma (measurable_rectangles ((Prod_Field (SubFin (S,k0))),(ElmFin (S,(k0 + 1))))) by A14, A15, Th21;
hence ex k being non zero Nat st
( k = n + 1 & PM . (n + 1) is sigma_Measure of (Prod_Field (SubFin (S,k))) ) by A15, A16, A17; :: thesis:

end;

end;

end;

A18: for n being Nat holds S₂[n] from NAT_1:sch 2(A4, A5);
for i being Nat st i in Seg m holds
ex Si being SigmaField of ((ProdFinSeq X) . i) st
( Si = (ProdSigmaFldFinSeq S) . i & PM . i is sigma_Measure of Si )

let i be Nat; :: thesis:
assume A19: i in Seg m ; :: thesis:
then A20: ( 1 <= i & i <= m ) by FINSEQ_1:1;
then consider k being non zero Nat such that
A21: ( k = i & PM . i is sigma_Measure of (Prod_Field (SubFin (S,k))) ) by A18;
reconsider Si = (ProdSigmaFldFinSeq S) . i as SigmaField of ((ProdFinSeq X) . i) by A19, Def2;
take Si ; :: thesis:
thus Si = (ProdSigmaFldFinSeq S) . i ; :: thesis:
A22: len X = m by CARD_1:def 7;
SubFin (X,m) = X | m by Def5;
then SubFin (X,m) = X by A22, FINSEQ_1:58;
then A23: CarProduct (SubFin (X,k)) = (ProdFinSeq X) . k by A21, A20, Th3;
Prod_Field (SubFin (S,k)) = (ProdSigmaFldFinSeq S) . k by A21, A20, Th20;
hence PM . i is sigma_Measure of Si by A21, A23; :: thesis:

end;

then reconsider PM = PM as sigmaMeasureFamily of ProdSigmaFldFinSeq S by Def8;
take PM ; :: thesis:
thus PM . 1 = M . 1 by A3; :: thesis:
thus for i being non zero Nat st i < m holds
ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( Mi = PM . i & PM . (i + 1) = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) :: thesis:

let i be non zero Nat; :: thesis:
assume A24: i < m ; :: thesis:
A25: 1 <= i by NAT_1:14;
then S₁[i,PM . i,PM . (i + 1)] by A3, A24;
hence ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( Mi = PM . i & PM . (i + 1) = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) by A18, A24, A25; :: thesis:

end;