theorem :: FIELD_16:58

for F being finite Field ex p being Prime ex n being non zero Nat st
( Char F = p & order F = p |^ n ) by finex2;