let m, n, k be non zero Nat; :: thesis: for X being non-empty m -element FinSequence
for S being sigmaFieldFamily of X st k <= n & n <= m holds
(ProdSigmaFldFinSeq S) . k = (ProdSigmaFldFinSeq (SubFin (S,n))) . k
let X be non-empty m -element FinSequence; :: thesis: for S being sigmaFieldFamily of X st k <= n & n <= m holds
(ProdSigmaFldFinSeq S) . k = (ProdSigmaFldFinSeq (SubFin (S,n))) . k
let S be sigmaFieldFamily of X; :: thesis: ( k <= n & n <= m implies (ProdSigmaFldFinSeq S) . k = (ProdSigmaFldFinSeq (SubFin (S,n))) . k )
assume that
A1: k <= n and
A2: n <= m ; :: thesis: (ProdSigmaFldFinSeq S) . k = (ProdSigmaFldFinSeq (SubFin (S,n))) . k
A3: SubFin (S,n) = S | n by A2, Def6;
A4: 1 <= k by NAT_1:14;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= n implies (ProdSigmaFldFinSeq S) . $1 = (ProdSigmaFldFinSeq (SubFin (S,n))) . $1 );
A5: S₁[ 0 ] ;
A6: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A7: S₁[i] ; :: thesis: S₁[i + 1]
assume A8: ( 1 <= i + 1 & i + 1 <= n ) ; :: thesis: (ProdSigmaFldFinSeq S) . (i + 1) = (ProdSigmaFldFinSeq (SubFin (S,n))) . (i + 1)

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

suppose A9: i = 0 ; :: thesis: (ProdSigmaFldFinSeq S) . (i + 1) = (ProdSigmaFldFinSeq (SubFin (S,n))) . (i + 1)

then A10: (ProdSigmaFldFinSeq S) . (i + 1) = S . 1 by Def11;
A11: (ProdSigmaFldFinSeq (SubFin (S,n))) . (i + 1) = (SubFin (S,n)) . 1 by A9, Def11;
1 <= n by A8, XXREAL_0:2;
then 1 in Seg n ;
hence (ProdSigmaFldFinSeq S) . (i + 1) = (ProdSigmaFldFinSeq (SubFin (S,n))) . (i + 1) by A3, A10, A11, FUNCT_1:49; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: (ProdSigmaFldFinSeq S) . (i + 1) = (ProdSigmaFldFinSeq (SubFin (S,n))) . (i + 1)

then reconsider i1 = i as non zero Nat ;
A12: i1 < n by A8, NAT_1:13;
then i1 < m by A2, XXREAL_0:2;
then A13: ex Si being SigmaField of (CarProduct (SubFin (X,i1))) st
( Si = (ProdSigmaFldFinSeq S) . i1 & (ProdSigmaFldFinSeq S) . (i1 + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i1 + 1))))) ) by Def11;
A14: ex Sj being SigmaField of (CarProduct (SubFin ((SubFin (X,n)),i1))) st
( Sj = (ProdSigmaFldFinSeq (SubFin (S,n))) . i1 & (ProdSigmaFldFinSeq (SubFin (S,n))) . (i1 + 1) = sigma (measurable_rectangles (Sj,(ElmFin ((SubFin (S,n)),(i1 + 1))))) ) by A12, Def11;
A15: ElmFin (S,(i1 + 1)) = ElmFin ((SubFin (S,n)),(i1 + 1)) by A2, A8, Th12;
ElmFin (X,(i1 + 1)) = ElmFin ((SubFin (X,n)),(i1 + 1)) by A2, A8, Th8;
hence (ProdSigmaFldFinSeq S) . (i + 1) = (ProdSigmaFldFinSeq (SubFin (S,n))) . (i + 1) by A7, A12, A13, A15, A14, A2, Th7, NAT_1:14; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A5, A6);
hence (ProdSigmaFldFinSeq S) . k = (ProdSigmaFldFinSeq (SubFin (S,n))) . k by A1, A4; :: thesis: verum