theorem Th60: :: UPROOTS:63

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
for c being Element 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
( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )