theorem :: E_TRANS1:36

for F being domRing
for E being domRingExtension of F
for p being Polynomial of F
for a being Element of F
for x, b being Element of E st b = a holds
Ext_eval ((a * p),x) = b * (Ext_eval (p,x))