let F be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F) holds
( NormPolynomial p is irreducible iff p is irreducible )
let p be Element of the carrier of (Polynom-Ring F); :: thesis: ( NormPolynomial p is irreducible iff p is irreducible )

now :: thesis: ( NormPolynomial p is irreducible implies p is irreducible )

assume B: NormPolynomial p is irreducible ; :: thesis: p is irreducible
NormPolynomial p is_associated_to p by np3;
hence p is irreducible by B, RING_2:23; :: thesis: verum

end;

hence ( NormPolynomial p is irreducible iff p is irreducible ) by np3, RING_2:23; :: thesis: verum