let p be Prime; :: thesis: for n being non zero Nat
for F being Field st card F = p |^ n holds
for a being Element of F holds a |^ (p |^ n) = a
let n be non zero Nat; :: thesis: for F being Field st card F = p |^ n holds
for a being Element of F holds a |^ (p |^ n) = a
let F be Field; :: thesis: ( card F = p |^ n implies for a being Element of F holds a |^ (p |^ n) = a )
assume A: card F = p |^ n ; :: thesis: for a being Element of F holds a |^ (p |^ n) = a
let a be Element of F; :: thesis: a |^ (p |^ n) = a
reconsider F = F as finite Field by A;
set M = MultGroup F;
reconsider n1 = n - 1 as Element of NAT by INT_1:3;
H: the carrier of F = the carrier of (MultGroup F) \/ {(0. F)} by UNIROOTS:15;

per cases ( a <> 0. F or a = 0. F ) ;

suppose a <> 0. F ; :: thesis: a |^ (p |^ n) = a

then not a in {(0. F)} by TARSKI:def 1;
then reconsider b = a as Element of (MultGroup F) by H, XBOOLE_0:def 3;
card (MultGroup F) = (p |^ n) - 1 by A, UNIROOTS:18;
then b * (b |^ ((p |^ n) - 1)) = b * (1_ (MultGroup F)) by GR_CY_1:9
.= a by GROUP_1:def 4 ;
hence a = b |^ (1 + ((p |^ n) - 1)) by GROUP_1:34
.= a |^ (p |^ n) by FIELD_15:10 ;
:: thesis: verum

end;

suppose a = 0. F ; :: thesis: a |^ (p |^ n) = a

hence a |^ (p |^ n) = a ; :: thesis: verum

end;

end;