let L be Field; :: thesis: for p being Polynomial of L st len p <> 0 holds
Roots p = Roots (NormPolynomial p)
let p be Polynomial of L; :: thesis: ( len p <> 0 implies Roots p = Roots (NormPolynomial p) )
assume A1: len p <> 0 ; :: thesis: Roots p = Roots (NormPolynomial p)
thus Roots p c= Roots (NormPolynomial p) :: according to XBOOLE_0:def 10 :: thesis: Roots (NormPolynomial p) c= Roots p

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Roots p or x in Roots (NormPolynomial p) )
assume A2: x in Roots p ; :: thesis: x in Roots (NormPolynomial p)
then reconsider x1 = x as Element of L ;
x1 is_a_root_of p by A2, Def10;
then x1 is_a_root_of NormPolynomial p by A1, Th59;
hence x in Roots (NormPolynomial p) by Def10; :: thesis: verum

end;

thus Roots (NormPolynomial p) c= Roots p :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Roots (NormPolynomial p) or x in Roots p )
assume A3: x in Roots (NormPolynomial p) ; :: thesis: x in Roots p
then reconsider x1 = x as Element of L ;
x1 is_a_root_of NormPolynomial p by A3, Def10;
then x1 is_a_root_of p by A1, Th59;
hence x in Roots p by Def10; :: thesis: verum

end;