:: deftheorem Def10 defines poly_with_roots UPROOTS:def 11 :
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b being bag of the carrier of L
for b₃ being Polynomial of L holds
( b₃ = poly_with_roots b iff ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b₃ = Product (FlattenSeq f) ) );