let F be finite Field; :: thesis: ex p being Prime ex n being non zero Nat st
( Char F = p & order F = p |^ n )
consider n being non zero Nat such that
A: card F = (Char F) |^ n by FIELD_15:92;
thus ex p being Prime ex n being non zero Nat st
( Char F = p & order F = p |^ n ) by A; :: thesis: verum