for R being domRing
for p being non constant Polynomial of R holds
( card (BRoots p) = deg p iff ex a being Element of R ex q being Ppoly of R st p = a * q )