let p be Prime; :: thesis: for n being non zero Nat
for F being Field st card F = p |^ n holds
Char F = p
let n be non zero Nat; :: thesis: for F being Field st card F = p |^ n holds
Char F = p
let F be Field; :: thesis: ( card F = p |^ n implies Char F = p )
assume AS: card F = p |^ n ; :: thesis: Char F = p
then B: F is finite ;
then consider n1 being non zero Nat such that
A: card F = (Char F) |^ n1 by FIELD_15:92;
thus Char F = p by A, B, AS, lemp; :: thesis: verum