let f, g be FinSequence of NAT ; :: thesis: ( len f = k & ( for i being Nat st i < k holds
f . (i + 1) = primenumber i ) & len g = k & ( for i being Nat st i < k holds
g . (i + 1) = primenumber i ) implies f = g )
assume that
A3: len f = k and
A4: for i being Nat st i < k holds
f . (i + 1) = primenumber i and
A5: len g = k and
A6: for i being Nat st i < k holds
g . (i + 1) = primenumber i ; :: thesis: f = g
thus len f = len g by A3, A5; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len f or f . b₁ = g . b₁ )
let i be Nat; :: thesis: ( not 1 <= i or not i <= len f or f . i = g . i )
assume that
A7: 1 <= i and
A8: i <= len f ; :: thesis: f . i = g . i
i - 1 >= 1 - 1 by A7, XREAL_1:9;
then A9: i = (i -' 1) + 1 by NAT_D:72;
i < k + 1 by A3, A8, NAT_1:13;
then A10: i - 1 < (k + 1) - 1 by XREAL_1:8;
hence f . i = primenumber (i -' 1) by A4, A9
.= g . i by A6, A9, A10 ;
:: thesis: verum