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
for T1 being RingExtension of S
for T2 being RingExtension of R st T1 = T2 holds
Roots (T2,p) = Roots (T1,q)