let n1, n be Nat; :: thesis: for p being Prime
for a being Element of (GF p) st a = n1 mod p holds
a |^ n = (n1 |^ n) mod p
let p be Prime; :: thesis: for a being Element of (GF p) st a = n1 mod p holds
a |^ n = (n1 |^ n) mod p
let a be Element of (GF p); :: thesis: ( a = n1 mod p implies a |^ n = (n1 |^ n) mod p )
P0: p > 1 by INT_2:def 4;
assume AS: a = n1 mod p ; :: thesis: a |^ n = (n1 |^ n) mod p
defpred S₁[ Nat] means (power (GF p)) . (a,$1) = (n1 |^ $1) mod p;
a |^ 0 = 1 by EX1;
then P1: a |^ 0 = 1 mod p by P0, NAT_D:63;
P2: S₁[ 0 ] by P1, NEWTON:4;

P3: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A0: S₁[n] ; :: thesis: S₁[n + 1]
reconsider b = (power (GF p)) . (a,n) as Element of (GF p) by EXLm1;
n - 0 is Element of NAT by NAT_1:21;
then (power (GF p)) . (a,(n + 1)) = b * a by GROUP_1:def 7
.= ((n1 |^ n) * n1) mod p by AS, A0, GF6
.= (n1 |^ (n + 1)) mod p by NEWTON:6 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P2, P3);
hence a |^ n = (n1 |^ n) mod p ; :: thesis: verum