theorem extevalsubst: :: FIELD_14:25

for F being Field
for p, q being Polynomial of F
for E being FieldExtension of F
for a being Element of E holds Ext_eval ((Subst (p,q)),a) = Ext_eval (p,(Ext_eval (q,a)))