for L being Field
for p being Polynomial of L st len p <> 0 holds
( p is with_roots iff NormPolynomial p is with_roots )