theorem r59a: :: FIELD_14:32

for F being Field
for S being non empty finite Subset of F
for a being Element of F
for p being Ppoly of F,(S \/ {a})
for q being non constant Polynomial of F st p = (rpoly (1,a)) *' q & not a in S holds
q is Ppoly of F,S