:: deftheorem defines SumRoots POLYVIE1:def 2 :
for L being domRing
for p being non-zero Polynomial of L holds SumRoots p = Sum ((BRoots p) (++) (canFS (Roots p)));