:: deftheorem Def1 defines primesFinS NUMBER13:def 1 :
for k being Nat
for b₂ being FinSequence of NAT holds
( b₂ = primesFinS k iff ( len b₂ = k & ( for i being Nat st i < k holds
b₂ . (i + 1) = primenumber i ) ) );