theorem :: RING_5:67

for R being domRing
for p, q being Polynomial of R st ex S being Subset of R st
( card S = (max ((deg p),(deg q))) + 1 & ( for a being Element of R st a in S holds
eval (p,a) = eval (q,a) ) ) holds
p = q