let m, n be non zero Nat; :: thesis: for X being non-empty m -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st n <= m holds
(ProdSigmaMesFinSeq M) . n = Prod_Measure (SubFin (M,n))
let X be non-empty m -element FinSequence; :: thesis: for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st n <= m holds
(ProdSigmaMesFinSeq M) . n = Prod_Measure (SubFin (M,n))
let S be sigmaFieldFamily of X; :: thesis: for M being sigmaMeasureFamily of S st n <= m holds
(ProdSigmaMesFinSeq M) . n = Prod_Measure (SubFin (M,n))
let M be sigmaMeasureFamily of S; :: thesis: ( n <= m implies (ProdSigmaMesFinSeq M) . n = Prod_Measure (SubFin (M,n)) )
assume A1: n <= m ; :: thesis: (ProdSigmaMesFinSeq M) . n = Prod_Measure (SubFin (M,n))
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= m implies ex k being non zero Nat st
( k = $1 & (ProdSigmaMesFinSeq M) . $1 = Prod_Measure (SubFin (M,k)) ) );
A2: S₁[ 0 ] ;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
assume A5: ( 1 <= i + 1 & i + 1 <= m ) ; :: thesis: ex k being non zero Nat st
( k = i + 1 & (ProdSigmaMesFinSeq M) . (i + 1) = Prod_Measure (SubFin (M,k)) )

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

suppose A6: i = 0 ; :: thesis: ex k being non zero Nat st
( k = i + 1 & (ProdSigmaMesFinSeq M) . (i + 1) = Prod_Measure (SubFin (M,k)) )

then (ProdSigmaMesFinSeq M) . (i + 1) = M . 1 by Def13;
then A7: (ProdSigmaMesFinSeq M) . (i + 1) = ElmFin (M,1) by A6, A5, Def10;
reconsider k = i + 1 as non zero Nat ;
Prod_Measure (SubFin (M,k)) = (SubFin (M,k)) . 1 by A6, Def13;
then Prod_Measure (SubFin (M,k)) = ElmFin ((SubFin (M,k)),1) by A6, Def10;
hence ex k being non zero Nat st
( k = i + 1 & (ProdSigmaMesFinSeq M) . (i + 1) = Prod_Measure (SubFin (M,k)) ) by A7, A5, Th17; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: ex k being non zero Nat st
( k = i + 1 & (ProdSigmaMesFinSeq M) . (i + 1) = Prod_Measure (SubFin (M,k)) )

then reconsider k0 = i as non zero Nat ;
k0 < m by A5, NAT_1:13;
then A8: ex Mk0 being sigma_Measure of (Prod_Field (SubFin (S,k0))) st
( Mk0 = (ProdSigmaMesFinSeq M) . k0 & (ProdSigmaMesFinSeq M) . (k0 + 1) = product_sigma_Measure (Mk0,(ElmFin (M,(k0 + 1)))) ) by Def13;
reconsider k = k0 + 1 as non zero Nat ;
A9: k0 < k by NAT_1:13;
then A10: ex Mk02 being sigma_Measure of (Prod_Field (SubFin ((SubFin (S,k)),k0))) st
( Mk02 = (ProdSigmaMesFinSeq (SubFin (M,k))) . k0 & (ProdSigmaMesFinSeq (SubFin (M,k))) . (k0 + 1) = product_sigma_Measure (Mk02,(ElmFin ((SubFin (M,k)),(k0 + 1)))) ) by Def13;
A11: SubFin (X,k0) = SubFin ((SubFin (X,k)),k0) by A5, A9, Th7;
A12: SubFin (S,k0) = SubFin ((SubFin (S,k)),k0) by A5, A9, Th14;
A13: ElmFin (X,(k0 + 1)) = ElmFin ((SubFin (X,k)),k) by A5, Th8;
A14: ElmFin (S,(k0 + 1)) = ElmFin ((SubFin (S,k)),k) by A5, Th12;
A15: ElmFin (M,(k0 + 1)) = ElmFin ((SubFin (M,k)),k) by A5, Th17;
(ProdSigmaMesFinSeq M) . (k0 + 1) = Prod_Measure (SubFin (M,k)) by A8, A15, A14, A13, A10, A11, A12, A9, A4, A5, NAT_1:13, NAT_1:14, Th23;
hence ex k being non zero Nat st
( k = i + 1 & (ProdSigmaMesFinSeq M) . (i + 1) = Prod_Measure (SubFin (M,k)) ) ; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
then S₁[n] ;
hence (ProdSigmaMesFinSeq M) . n = Prod_Measure (SubFin (M,n)) by A1, NAT_1:14; :: thesis: verum