let f, g be FinSequence of NAT ; :: thesis: ( len f = s & ( for k being non zero Nat st k <= s holds
f . k = (((sequenceA s) . k) + 1) / (primenumber (k - 1)) ) & len g = s & ( for k being non zero Nat st k <= s holds
g . k = (((sequenceA s) . k) + 1) / (primenumber (k - 1)) ) implies f = g )
assume that
A6: len f = s and
A7: for k being non zero Nat st k <= s holds
f . k = H₁(k) and
A8: len g = s and
A9: for k being non zero Nat st k <= s holds
g . k = H₁(k) ; :: thesis: f = g
thus len f = len g by A6, A8; :: 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 k be Nat; :: thesis: ( not 1 <= k or not k <= len f or f . k = g . k )
assume that
A10: 1 <= k and
A11: k <= len f ; :: thesis: f . k = g . k
reconsider k = k as non zero Nat by A10;
f . k = H₁(k) by A6, A7, A11
.= g . k by A6, A9, A11 ;
hence f . k = g . k ; :: thesis: verum