theorem copr2: :: FIELD_12:5

for F being Field
for p, q being Element of the carrier of (Polynom-Ring F) st p,q are_coprime holds
p,q have_no_common_roots