:: deftheorem Def10 defines sequenceAnPk NUMBER15:def 10 :
for s being Nat
for k being non zero Nat st k <= s holds
for b₃ being FinSequence of NAT holds
( b₃ = sequenceAnPk (s,k) iff ( len b₃ = s & ( for n being non zero Nat st n <= s holds
( ( n <> k implies b₃ . n = ((sequenceA s) . n) / (primenumber (k - 1)) ) & ( n = k implies b₃ . n = 0 ) ) ) ) );