let S1, S2 be sigmaFieldFamily of ProdFinSeq X; :: thesis: ( S1 . 1 = S . 1 & ( for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = S1 . i & S1 . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) ) & S2 . 1 = S . 1 & ( for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = S2 . i & S2 . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) ) implies S1 = S2 )
assume that
A24: ( S1 . 1 = S . 1 & ( for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = S1 . i & S1 . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) ) ) and
A25: ( S2 . 1 = S . 1 & ( for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = S2 . i & S2 . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) ) ) ; :: thesis: S1 = S2
A26: ( len S1 = m & len S2 = m ) by CARD_1:def 7;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= m implies S1 . $1 = S2 . $1 );
A27: S₁[ 0 ] ;
A28: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A29: S₁[k] ; :: thesis: S₁[k + 1]
assume A30: ( 1 <= k + 1 & k + 1 <= m ) ; :: thesis: S1 . (k + 1) = S2 . (k + 1)

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: S1 . (k + 1) = S2 . (k + 1)

hence S1 . (k + 1) = S2 . (k + 1) by A24, A25; :: thesis: verum

end;

suppose A31: k <> 0 ; :: thesis: S1 . (k + 1) = S2 . (k + 1)

then reconsider j = k as non zero Nat ;
k + 1 <> 1 by A31;
then A32: 1 < k + 1 by A30, XXREAL_0:1;
A33: ex Si being SigmaField of (CarProduct (SubFin (X,j))) st
( Si = S1 . j & S1 . (j + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(j + 1))))) ) by A24, A30, NAT_1:13;
ex Si being SigmaField of (CarProduct (SubFin (X,j))) st
( Si = S2 . j & S2 . (j + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(j + 1))))) ) by A25, A30, NAT_1:13;
hence S1 . (k + 1) = S2 . (k + 1) by A33, A29, A32, A30, NAT_1:13; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A27, A28);
hence S1 = S2 by A26; :: thesis: verum