theorem Th22: :: POLYVIE1:22

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)
for P being Permutation of (dom E) holds ((BRoots (<%a,b%> *' p)) (++) E) * P = (BRoots (<%a,b%> *' p)) (++) (E * P)