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

proof

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

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

suppose n = 0 ; :: thesis: (ProdFinSeq (SubFin (X,j))) . (n + 1) = (ProdFinSeq (SubFin (X,k))) . (n + 1)

then ( (ProdFinSeq (SubFin (X,j))) . (n + 1) = (SubFin (X,j)) . 1 & (ProdFinSeq (SubFin (X,k))) . (n + 1) = (SubFin (X,k)) . 1 ) by Def3;
then ( (ProdFinSeq (SubFin (X,j))) . (n + 1) = (X | j) . 1 & (ProdFinSeq (SubFin (X,k))) . (n + 1) = (X | k) . 1 ) by A2, A3, Def5, XXREAL_0:2;
then ( (ProdFinSeq (SubFin (X,j))) . (n + 1) = X . 1 & (ProdFinSeq (SubFin (X,k))) . (n + 1) = X . 1 ) by A4, FUNCT_1:49;
hence (ProdFinSeq (SubFin (X,j))) . (n + 1) = (ProdFinSeq (SubFin (X,k))) . (n + 1) ; :: thesis: verum

end;

suppose A9: n <> 0 ; :: thesis: (ProdFinSeq (SubFin (X,j))) . (n + 1) = (ProdFinSeq (SubFin (X,k))) . (n + 1)

then reconsider n1 = n as non zero Nat ;
A10: 1 <= n by A9, NAT_1:14;
A11: n < j by A8, NAT_1:13;
n + 1 <= k by A8, A2, XXREAL_0:2;
then A12: ( n + 1 in Seg j & n + 1 in Seg k ) by A8;
( SubFin (X,j) = X | j & SubFin (X,k) = X | k ) by A2, A3, Def5, XXREAL_0:2;
then A13: ( (SubFin (X,j)) . (n + 1) = X . (n + 1) & (SubFin (X,k)) . (n + 1) = X . (n + 1) ) by A12, FUNCT_1:49;
reconsider j1 = j - 1 as non zero Nat by A9, A8, NAT_1:13, NAT_1:14, NAT_1:20;
1 < j by A10, A11, XXREAL_0:2;
then 1 < k by A2, XXREAL_0:2;
then reconsider k1 = k - 1 as Nat by NAT_1:20;
j1 <= k1 by A2, XREAL_1:9;
then reconsider k1 = k1 as non zero Nat ;
A14: n1 < k1 + 1 by A2, A11, XXREAL_0:2;
(ProdFinSeq (SubFin (X,(j1 + 1)))) . (n1 + 1) = [:((ProdFinSeq (SubFin (X,(k1 + 1)))) . n),((SubFin (X,(k1 + 1))) . (n1 + 1)):] by A13, A11, A7, Def3, NAT_1:14;
hence (ProdFinSeq (SubFin (X,j))) . (n + 1) = (ProdFinSeq (SubFin (X,k))) . (n + 1) by A14, Def3; :: thesis: verum

end;

end;

end;

A15: for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A6);
1 <= i by NAT_1:14;
hence (ProdFinSeq (SubFin (X,j))) . i = (ProdFinSeq (SubFin (X,k))) . i by A1, A15; :: thesis: verum