let n, i, j, k be non zero Nat; :: thesis: for X being n -element FinSequence
for X1 being j -element FinSequence
for X2 being k -element FinSequence st i <= j & j <= k & X1 = X | j & X2 = X | k holds
(ProdFinSeq X1) . i = (ProdFinSeq X2) . i
let X be n -element FinSequence; :: thesis: for X1 being j -element FinSequence
for X2 being k -element FinSequence st i <= j & j <= k & X1 = X | j & X2 = X | k holds
(ProdFinSeq X1) . i = (ProdFinSeq X2) . i
let X1 be j -element FinSequence; :: thesis: for X2 being k -element FinSequence st i <= j & j <= k & X1 = X | j & X2 = X | k holds
(ProdFinSeq X1) . i = (ProdFinSeq X2) . i
let X2 be k -element FinSequence; :: thesis: ( i <= j & j <= k & X1 = X | j & X2 = X | k implies (ProdFinSeq X1) . i = (ProdFinSeq X2) . i )
assume that
A1: i <= j and
A2: j <= k and
A3: X1 = X | j and
A4: X2 = X | k ; :: thesis: (ProdFinSeq X1) . i = (ProdFinSeq X2) . i
defpred S₁[ non zero Nat] means ( $1 <= j implies (ProdFinSeq X1) . $1 = (ProdFinSeq X2) . $1 );
A5: S₁[1]

proof

assume A6: 1 <= j ; :: thesis: (ProdFinSeq X1) . 1 = (ProdFinSeq X2) . 1
(ProdFinSeq X1) . 1 = X1 . 1 by MEASUR13:def 3;
then A7: (ProdFinSeq X1) . 1 = X . 1 by A3, A6, FINSEQ_3:112;
(ProdFinSeq X2) . 1 = X2 . 1 by MEASUR13:def 3;
hence (ProdFinSeq X1) . 1 = (ProdFinSeq X2) . 1 by A4, A7, A6, A2, XXREAL_0:2, FINSEQ_3:112; :: thesis: verum

end;

A8: for m being non zero Nat st S₁[m] holds
S₁[m + 1]

proof

let m be non zero Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A9: S₁[m] ; :: thesis: S₁[m + 1]
assume A10: m + 1 <= j ; :: thesis: (ProdFinSeq X1) . (m + 1) = (ProdFinSeq X2) . (m + 1)
then A11: m < j by NAT_1:13;
then A12: m < k by A2, XXREAL_0:2;
A13: ( X1 . (m + 1) = X . (m + 1) & X2 . (m + 1) = X . (m + 1) ) by A2, A3, A4, A10, FINSEQ_3:112, XXREAL_0:2;
(ProdFinSeq X1) . (m + 1) = [:((ProdFinSeq X1) . m),(X1 . (m + 1)):] by A11, MEASUR13:def 3;
hence (ProdFinSeq X1) . (m + 1) = (ProdFinSeq X2) . (m + 1) by A13, A9, A10, A12, NAT_1:13, MEASUR13:def 3; :: thesis: verum

end;

for m being non zero Nat holds S₁[m] from NAT_1:sch 10(A5, A8);
hence (ProdFinSeq X1) . i = (ProdFinSeq X2) . i by A1; :: thesis: verum