let K be F -extending E -finite FieldExtension of F; :: thesis: K is F -finite
set BE = the Basis of (VecSp (E,F));
set BK = the Basis of (VecSp (K,E));
Base ( the Basis of (VecSp (E,F)), the Basis of (VecSp (K,E))) is Basis of (VecSp (K,F)) by BasKEF;
then VecSp (K,F) is finite-dimensional by MATRLIN:def 1;
hence K is F -finite by FIELD_4:def 8; :: thesis: verum