theorem r59: :: FIELD_14:33

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