for L being non degenerated comRing
for r being Element of L
for p being non-zero Polynomial of L st r is_a_root_of p holds
len (poly_quotient (p,r)) > 0