let p be Prime; :: thesis: for F being finite p -characteristic Field
for a being Element of F ex b being Element of F st b |^ p = a
let F be finite p -characteristic Field; :: thesis: for a being Element of F ex b being Element of F st b |^ p = a
let a be Element of F; :: thesis: ex b being Element of F st b |^ p = a
set M = MultGroup F;
Char F = p by RING_3:def 6;
then consider n being non zero Nat such that
A: card F = p |^ n by CF;
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: ex b being Element of F st b |^ p = 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 |^ ((p |^ n) - 1) = 1_ (MultGroup F) by GR_CY_1:9;
then (1_ (MultGroup F)) * b = (b |^ ((p |^ n) - 1)) * (b |^ 1) by GROUP_1:26
.= b |^ (((p |^ n) - 1) + 1) by GROUP_1:33
.= a |^ (p |^ (n1 + 1)) by MG
.= a |^ ((p |^ n1) * p) by NEWTON:6
.= (a |^ (p |^ n1)) |^ p by BINOM:11 ;
then a = (a |^ (p |^ n1)) |^ p by GROUP_1:def 4;
hence ex b being Element of F st b |^ p = a ; :: thesis: verum

end;

suppose C: a = 0. F ; :: thesis: ex b being Element of F st b |^ p = a

(0. F) |^ p = 0. F ;
hence ex b being Element of F st b |^ p = a by C; :: thesis: verum

end;

end;