theorem np3: :: RING_4:27

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