:: deftheorem Def9 defines fpoly_mult_root UPROOTS:def 10 :
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for c being Element of L
for n being Element of NAT
for b₄ being FinSequence of (Polynom-Ring L) holds
( b₄ = fpoly_mult_root (c,n) iff ( len b₄ = n & ( for i being Element of NAT st i in dom b₄ holds
b₄ . i = <%(- c),(1. L)%> ) ) );