theorem fixeval: :: FIELD_13:42

for F being Field
for E being FieldExtension of F
for K being FieldExtension of E
for p being Element of the carrier of (Polynom-Ring F)
for a being Element of E
for h being b₁ -fixing Homomorphism of E,K holds h . (Ext_eval (p,a)) = Ext_eval (p,(h . a))