for R being domRing
for p being non zero with_roots Polynomial of R ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p )