:: deftheorem Def9 defines sequenceAk1Pk NUMBER15:def 9 :
for s being Nat
for b₂ being FinSequence of NAT holds
( b₂ = sequenceAk1Pk s iff ( len b₂ = s & ( for k being non zero Nat st k <= s holds
b₂ . k = (((sequenceA s) . k) + 1) / (primenumber (k - 1)) ) ) );