:: deftheorem defines Phi FIELD_8:def 9 :
for F being Field
for E being FieldExtension of F
for a, b being b₁ -algebraic Element of E holds Phi (a,b) = { [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } ;