for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b being bag of the carrier of L
for f being FinSequence of the carrier of (Polynom-Ring L) *
for 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))) ) holds
len (FlattenSeq f) = degree b