theorem ZZ1a: :: FIELD_14:31

for F being Field
for S being non empty finite Subset of F
for p being Ppoly of F,S
for q being non zero with_roots Polynomial of F st p *' q is Ppoly of F,(S \/ (Roots q)) holds
q is Ppoly of F,(Roots q)