let p be Prime; :: thesis: for n being non zero Nat
for F being Field st card F = p |^ n holds
card (PrimeField F) = p
let n be non zero Nat; :: thesis: for F being Field st card F = p |^ n holds
card (PrimeField F) = p
let K be Field; :: thesis: ( card K = p |^ n implies card (PrimeField K) = p )
assume AS: card K = p |^ n ; :: thesis: card (PrimeField K) = p
Char K = p by AS, T5;
then reconsider F = K as finite p -characteristic Field by AS, RING_3:def 6;
PrimeField F, Z/ p are_isomorphic by RING_3:108;
then consider i being Function of (PrimeField F),(Z/ p) such that
B: i is isomorphism ;
C: dom i = the carrier of (PrimeField F) by FUNCT_2:def 1;
rng i = the carrier of (Z/ p) by B, FUNCT_2:def 3;
hence card (PrimeField K) = card (Z/ p) by C, B, CARD_1:70
.= p by fresh3a ;
:: thesis: verum