theorem Th46: :: UPROOTS:49

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