theorem :: FIELD_7:32

for F being Field
for E being FieldExtension of F holds
( E is F -algebraic iff for a being Element of E holds FAdj (F,{a}) is F -finite )