let m, n, k 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 k <= n & n <= m holds
(ProdSigmaMesFinSeq (SubFin (M,n))) . k = (ProdSigmaMesFinSeq (SubFin (M,k))) . k
let X be non-empty m -element FinSequence; :: thesis: for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st k <= n & n <= m holds
(ProdSigmaMesFinSeq (SubFin (M,n))) . k = (ProdSigmaMesFinSeq (SubFin (M,k))) . k
let S be sigmaFieldFamily of X; :: thesis: for M being sigmaMeasureFamily of S st k <= n & n <= m holds
(ProdSigmaMesFinSeq (SubFin (M,n))) . k = (ProdSigmaMesFinSeq (SubFin (M,k))) . k
let M be sigmaMeasureFamily of S; :: thesis: ( k <= n & n <= m implies (ProdSigmaMesFinSeq (SubFin (M,n))) . k = (ProdSigmaMesFinSeq (SubFin (M,k))) . k )
assume that
A1: k <= n and
A2: n <= m ; :: thesis: (ProdSigmaMesFinSeq (SubFin (M,n))) . k = (ProdSigmaMesFinSeq (SubFin (M,k))) . k
A3: k <= m by A1, A2, XXREAL_0:2;
A4: ( 1 <= n & 1 <= k ) by NAT_1:14;

now :: thesis: ( k <> n implies (ProdSigmaMesFinSeq (SubFin (M,n))) . k = (ProdSigmaMesFinSeq (SubFin (M,k))) . k )

assume k <> n ; :: thesis: (ProdSigmaMesFinSeq (SubFin (M,n))) . k = (ProdSigmaMesFinSeq (SubFin (M,k))) . k
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= k implies (ProdSigmaMesFinSeq (SubFin (M,n))) . $1 = (ProdSigmaMesFinSeq (SubFin (M,k))) . $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 <= k ) ; :: thesis: (ProdSigmaMesFinSeq (SubFin (M,n))) . (i + 1) = (ProdSigmaMesFinSeq (SubFin (M,k))) . (i + 1)

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

suppose i = 0 ; :: thesis: (ProdSigmaMesFinSeq (SubFin (M,n))) . (i + 1) = (ProdSigmaMesFinSeq (SubFin (M,k))) . (i + 1)

then A9: ( (ProdSigmaMesFinSeq (SubFin (M,n))) . (i + 1) = (SubFin (M,n)) . 1 & (ProdSigmaMesFinSeq (SubFin (M,k))) . (i + 1) = (SubFin (M,k)) . 1 ) by Def13;
( 1 in Seg n & 1 in Seg k ) by A4;
then ( (M | n) . 1 = M . 1 & (M | k) . 1 = M . 1 ) by FUNCT_1:49;
then ( (SubFin (M,n)) . 1 = M . 1 & (SubFin (M,k)) . 1 = M . 1 ) by A1, A2, Def9, XXREAL_0:2;
hence (ProdSigmaMesFinSeq (SubFin (M,n))) . (i + 1) = (ProdSigmaMesFinSeq (SubFin (M,k))) . (i + 1) by A9; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: (ProdSigmaMesFinSeq (SubFin (M,n))) . (i + 1) = (ProdSigmaMesFinSeq (SubFin (M,k))) . (i + 1)

then reconsider i0 = i as non zero Nat ;
A10: i0 < k by A8, NAT_1:13;
then A11: i0 < n by A1, XXREAL_0:2;
then A12: ex M1 being sigma_Measure of (Prod_Field (SubFin ((SubFin (S,n)),i0))) st
( M1 = (ProdSigmaMesFinSeq (SubFin (M,n))) . i0 & (ProdSigmaMesFinSeq (SubFin (M,n))) . (i0 + 1) = product_sigma_Measure (M1,(ElmFin ((SubFin (M,n)),(i0 + 1)))) ) by Def13;
A13: ex M2 being sigma_Measure of (Prod_Field (SubFin ((SubFin (S,k)),i0))) st
( M2 = (ProdSigmaMesFinSeq (SubFin (M,k))) . i0 & (ProdSigmaMesFinSeq (SubFin (M,k))) . (i0 + 1) = product_sigma_Measure (M2,(ElmFin ((SubFin (M,k)),(i0 + 1)))) ) by A10, Def13;
CarProduct (SubFin ((SubFin (X,n)),i0)) = CarProduct (SubFin (X,i0)) by A2, A11, Th7;
then A14: CarProduct (SubFin ((SubFin (X,n)),i0)) = CarProduct (SubFin ((SubFin (X,k)),i0)) by A3, A10, Th7;
SubFin ((SubFin (X,n)),i0) = SubFin (X,i0) by A2, A11, Th7;
then A15: SubFin ((SubFin (X,n)),i0) = SubFin ((SubFin (X,k)),i0) by A3, A10, Th7;
SubFin ((SubFin (S,n)),i0) = SubFin (S,i0) by A2, A11, Th14;
then A16: Prod_Field (SubFin ((SubFin (S,n)),i0)) = Prod_Field (SubFin ((SubFin (S,k)),i0)) by A15, A3, A10, Th14;
A17: i0 + 1 <= n by A8, A1, XXREAL_0:2;
then ElmFin ((SubFin (X,n)),(i0 + 1)) = ElmFin (X,(i0 + 1)) by A2, Th8;
then A18: ElmFin ((SubFin (X,n)),(i0 + 1)) = ElmFin ((SubFin (X,k)),(i0 + 1)) by A3, A8, Th8;
ElmFin ((SubFin (S,n)),(i0 + 1)) = ElmFin (S,(i0 + 1)) by A17, A2, Th12;
then A19: ElmFin ((SubFin (S,n)),(i0 + 1)) = ElmFin ((SubFin (S,k)),(i0 + 1)) by A3, A8, Th12;
ElmFin ((SubFin (M,n)),(i0 + 1)) = ElmFin (M,(i0 + 1)) by A17, A2, Th17;
hence (ProdSigmaMesFinSeq (SubFin (M,n))) . (i + 1) = (ProdSigmaMesFinSeq (SubFin (M,k))) . (i + 1) by A7, A12, A13, A19, A18, A16, A14, A3, A8, Th17, NAT_1:13, NAT_1:14; :: thesis: verum

end;

end;

end;

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

end;

hence (ProdSigmaMesFinSeq (SubFin (M,n))) . k = (ProdSigmaMesFinSeq (SubFin (M,k))) . k ; :: thesis: verum