theorem simpAgcd: :: FIELD_14:53
for F being Field
for S1, S2 being non empty finite Subset of F
for p1 being Ppoly of F,S1
for p2 being Polynomial of F st S2 = S1 /\ (Roots p2) holds
p1 gcd p2 is Ppoly of F,S2