:: deftheorem Def8 defines BRoots UPROOTS:def 9 :
for L being domRing
for p being non-zero Polynomial of L
for b₃ being bag of the carrier of L holds
( b₃ = BRoots p iff ( support b₃ = Roots p & ( for x being Element of L holds b₃ . x = multiplicity (p,x) ) ) );