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 S1[ 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: S1[ 0 ] by A3, NEWTON:4;
A5: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A6: S1[n] ; :: thesis: S1[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 S1[n + 1] ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A4, A5);
 hence a |^ n = (n1 |^ n) mod p ; :: thesis: verum