theorem Th25: :: POLYVIE1:25

for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L
for E being Enumeration of Roots (<%a,b%> *' p) holds Sum ((BRoots <%a,b%>) (++) E) = - (a / b)