theorem thirr2: :: RING_4:28

for F being Field
for p being Element of the carrier of (Polynom-Ring F) holds
( NormPolynomial p is irreducible iff p is irreducible )