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
deg p = deg q