theorem main1: :: FIELD_15:81

for F being Field
for p being non constant irreducible Element of the carrier of (Polynom-Ring F) holds
( p is separable iff (Deriv F) . p <> 0_. F )