for R being domRing
for S being domRingExtension of R
for p being non zero Element of the carrier of (Polynom-Ring R)
for h being b₁ -fixing Monomorphism of S holds h | (Roots (S,p)) is Permutation of (Roots (S,p))