theorem :: POLYNOM9:85

ex Poly being INT -valued Polynomial of 10,F_Real st
for k being positive Nat holds
( k + 1 is prime iff ex v being natural-valued Function of 10,F_Real st
( v . 1 = k & eval (Poly,v) = 0. F_Real ) )