for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E
for x being Element of F holds x = Ext_eval ((x | F),a)