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

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

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

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

end;

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

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

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

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

end;

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

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

end;

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

end;

end;