theorem prm: :: FIELD_8:38

for R being Ring
for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R)
for h being b₁ -fixing Monomorphism of S
for a being Element of S holds
( a in Roots (S,p) iff h . a in Roots (S,p) )