for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E
for p being Polynomial of F holds Ext_eval (p,a) in Lin (Base a)