let L be Field; :: thesis: for p being Polynomial of L st len p <> 0 holds
( p is with_roots iff NormPolynomial p is with_roots )
let p be Polynomial of L; :: thesis: ( len p <> 0 implies ( p is with_roots iff NormPolynomial p is with_roots ) )
assume A1: len p <> 0 ; :: thesis: ( p is with_roots iff NormPolynomial p is with_roots )
thus ( p is with_roots implies NormPolynomial p is with_roots ) :: thesis: ( NormPolynomial p is with_roots implies p is with_roots )

proof

assume p is with_roots ; :: thesis: NormPolynomial p is with_roots
then consider x being Element of L such that
A2: x is_a_root_of p ;
x is_a_root_of NormPolynomial p by A1, A2, Th59;
hence NormPolynomial p is with_roots ; :: thesis: verum

end;

assume NormPolynomial p is with_roots ; :: thesis: p is with_roots
then consider x being Element of L such that
A3: x is_a_root_of NormPolynomial p ;
x is_a_root_of p by A1, A3, Th59;
hence p is with_roots ; :: thesis: verum