theorem :: POLYVIE1:30

for L being algebraic-closed Field
for p, q being non-zero Polynomial of L st len p >= 2 holds
SumRoots (p *' q) = (SumRoots p) + (SumRoots q)