let p be Prime; :: thesis: for a being Element of (Z/ p) holds a |^ p = a
let a be Element of (Z/ p); :: thesis: a |^ p = a
set F = Z/ p;
set M = MultGroup (Z/ p);
H: the carrier of (Z/ p) = the carrier of (MultGroup (Z/ p)) \/ {(0. (Z/ p))} by UNIROOTS:15;
Char (Z/ p) = p by RING_3:def 6;
then consider n being non zero Nat such that
A: card (Z/ p) = p |^ n by FIELD_15:92;

I: now :: thesis: not n <> 1

assume J: n <> 1 ; :: thesis: contradiction
n >= 0 + 1 by INT_1:7;
then n > 1 by J, XXREAL_0:1;
then p |^ n > p |^ 1 by NAT_6:2;
hence contradiction by A, fresh3a; :: thesis: verum

end;

per cases ( a <> 0. (Z/ p) or a = 0. (Z/ p) ) ;

suppose a <> 0. (Z/ p) ; :: thesis: a |^ p = a

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

end;

suppose a = 0. (Z/ p) ; :: thesis: a |^ p = a

hence a |^ p = a ; :: thesis: verum

end;

end;