Base a is Basis of (VecSp ((FAdj (F,{a})),F)) by lembas;
then VecSp ((FAdj (F,{a})),F) is finite-dimensional by MATRLIN:def 1;
hence FAdj (F,{a}) is F -finite by FIELD_4:def 8; :: thesis: verum