let F be finite Field; :: thesis: F is PrimeField F -finite FieldExtension of PrimeField F
set P = PrimeField F;
reconsider E = F as FieldExtension of PrimeField F by FIELD_4:7;
the carrier of E = the carrier of (VecSp (E,(PrimeField F))) by FIELD_4:def 6;
then [#] (VecSp (E,(PrimeField F))) is finite ;
then VecSp (E,(PrimeField F)) is finite-dimensional by RANKNULL:4;
hence F is PrimeField F -finite FieldExtension of PrimeField F by FIELD_4:def 8; :: thesis: verum