theorem :: FIELD_4:27

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)
for a being Element of R
for b being Element of S st q = p & b = a holds
eval (q,b) = eval (p,a)