theorem :: POLYVIE1:31

for L being algebraic-closed domRing
for p being non-zero Polynomial of L
for r being FinSequence of L st r is one-to-one & len r = (len p) -' 1 & Roots p = rng r holds
Sum r = SumRoots p