theorem Th23: :: POLYVIE1:23

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
((canFS (Roots (<%a,b%> *' p))) ") * E is Permutation of (dom E)