for L being non trivial comRing
for s being non empty finite Subset of L
for x being Element of L
for f being FinSequence of L st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = eval (<%(- c),(1. L)%>,x) ) holds
eval ((poly_with_roots ((s,1) -bag)),x) = Product f