theorem Th16: :: POLYVIE1:16

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
(canFS (Roots p)) ^ <*(- (a / b))*> is Enumeration of Roots (<%a,b%> *' p)