let F be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F) holds NormPolynomial p is_associated_to p
let p be Element of the carrier of (Polynom-Ring F); :: thesis: NormPolynomial p is_associated_to p
reconsider a = p, b = NormPolynomial p as Element of (Polynom-Ring F) ;
A: p *' (1_. F) = p by POLYNOM3:35;
then B: p divides NormPolynomial p by T2, np2;
NormPolynomial p divides p by A, np1, T2;
hence NormPolynomial p is_associated_to p by B; :: thesis: verum