set p = the irreducible Element of the carrier of (Polynom-Ring F);
set q = NormPolynomial the irreducible Element of the carrier of (Polynom-Ring F);
take NormPolynomial the irreducible Element of the carrier of (Polynom-Ring F) ; :: thesis: ( NormPolynomial the irreducible Element of the carrier of (Polynom-Ring F) is monic & NormPolynomial the irreducible Element of the carrier of (Polynom-Ring F) is irreducible )
thus ( NormPolynomial the irreducible Element of the carrier of (Polynom-Ring F) is monic & NormPolynomial the irreducible Element of the carrier of (Polynom-Ring F) is irreducible ) by RING_4:28; :: thesis: verum