theorem Th24: :: POLYVIE1:24

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 st not - (a / b) in Roots p holds
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
Sum ((BRoots (<%a,b%> *' p)) (++) E) = Sum ((BRoots (<%a,b%> *' p)) (++) (canFS (Roots (<%a,b%> *' p))))