reconsider K = E as F -extending FieldExtension of F by FIELD_4:6;
take K ; :: thesis: K is E -finite
the carrier of K = the carrier of E ;
then deg (K,E) = 1 by quah1;
then {(1. K)} is Basis of (VecSp (K,E)) by quah2;
then VecSp (K,E) is finite-dimensional by MATRLIN:def 1;
hence K is E -finite by FIELD_4:def 8; :: thesis: verum