:: deftheorem defines deg FIELD_14:def 9 :
for F being Field
for E being FieldExtension of F
for a being Element of E holds deg (a,F) = deg ((FAdj (F,{a})),F);