let F be finite Field; :: thesis: card (PrimeField F) = Char F
consider p being Prime, n being non zero Nat such that
A: ( Char F = p & order F = p |^ n ) by finex2;
thus card (PrimeField F) = Char F by A, Ffix1; :: thesis: verum