let n, n1 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 )
A1: p > 1 by INT_2:def 4;
assume A2: 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 Th21;
then A3: a |^ 0 = 1 mod p by A1, NAT_D:63;
A4: S₁[ 0 ] by A3, NEWTON:4;

A5: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
reconsider b = (power (GF p)) . (a,n) as Element of (GF p) ;
(power (GF p)) . (a,(n + 1)) = b * a by GROUP_1:def 7
.= ((n1 |^ n) * n1) mod p by A2, A6, Th18
.= (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(A4, A5);
hence a |^ n = (n1 |^ n) mod p ; :: thesis: verum