theorem :: UPROOTS:65

for L being algebraic-closed domRing
for p being non-zero Polynomial of L st p . ((len p) -' 1) = 1. L holds
p = poly_with_roots (BRoots p)