theorem :: NUMBER19:67

for n being Nat ex p, q being Polynomial of INT.Ring st
( degree p > 0 & degree q > 0 & ( for i being Nat st i <= n holds
eval ((p *' q),(In ((primenumber i),INT.Ring))) = primenumber i ) )