let F be GaloisField of p |^ n; :: thesis: ( F is Z/ p -finite & F is Z/ p -simple )
set V = VecSp (F,(Z/ p));
[#] (VecSp (F,(Z/ p))) = the carrier of F by FIELD_4:def 6;
then VecSp (F,(Z/ p)) is finite-dimensional by RANKNULL:4;
hence F is Z/ p -finite by FIELD_4:def 8; :: thesis: F is Z/ p -simple
hence F is Z/ p -simple ; :: thesis: verum