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

per cases ( p = 0_. F or p <> 0_. F ) ;

suppose p = 0_. F ; :: thesis: ( q divides p iff q divides NormPolynomial p )

hence ( q divides p iff q divides NormPolynomial p ) by npl0; :: thesis: verum

end;

suppose AS: p <> 0_. F ; :: thesis: ( q divides p iff q divides NormPolynomial p )

then AS1: not p is zero by UPROOTS:def 5;

A: now :: thesis: ( q divides p implies q divides NormPolynomial p )

assume q divides p ; :: thesis: q divides NormPolynomial p
then consider r being Polynomial of F such that
A1: p = q *' r by T2;
set a = (LC p) " ;
NormPolynomial p = ((LC p) ") * (q *' r) by AS1, A1, npl
.= q *' (((LC p) ") * r) by poly2 ;
hence q divides NormPolynomial p by T2; :: thesis: verum

end;

now :: thesis: ( q divides NormPolynomial p implies q divides p )

assume q divides NormPolynomial p ; :: thesis: q divides p
then consider r being Polynomial of F such that
A1: NormPolynomial p = q *' r by T2;
set a = (LC p) " ;
not p is zero by AS, UPROOTS:def 5;
then LC p <> 0. F ;
then ((LC p) ") * (LC p) = 1. F by VECTSP_1:def 10;
then (LC p) " <> 0. F ;
then (((LC p) ") ") * ((LC p) ") = 1. F by VECTSP_1:def 10;
then p = ((((LC p) ") ") * ((LC p) ")) * p by poly2a
.= (((LC p) ") ") * (((LC p) ") * p) by poly3
.= (((LC p) ") ") * (q *' r) by AS1, A1, npl
.= q *' ((((LC p) ") ") * r) by poly2 ;
hence q divides p by T2; :: thesis: verum

end;

hence ( q divides p iff q divides NormPolynomial p ) by A; :: thesis: verum

end;

end;