theorem :: UPROOTS:51

for L being non degenerated comRing
for r being Element of L
for p, q being Polynomial of L st p = <%(- r),(1. L)%> *' q holds
r is_a_root_of p