theorem m4: :: FIELD_7:13

for R being Ring
for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S) st p = q holds
Roots (S,p) = Roots q