theorem lem20: :: REALALG3:16

for F being Field
for E being FieldExtension 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))