theorem :: POLYNOM5:61
for L being Field
for p being Polynomial of L st len p <> 0 holds
Roots p = Roots (NormPolynomial p)