:: deftheorem Def3 defines PrimeNumbersS NUMBER15:def 3 :
for s being Nat
for b₂ being sequence of SetPrimes holds
( b₂ = PrimeNumbersS s iff for n being Nat holds b₂ . n = primenumber n );