:: deftheorem Def7 defines -finite FIELD_4:def 8 :
for F being Field
for E being FieldExtension of F holds
( E is F -finite iff VecSp (E,F) is finite-dimensional );