theorem mm6: :: FIELD_14:70

for F being 0 -characteristic Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds p gcd ((Deriv F) . p) = 1_. F