let n be Nat; :: thesis: for p being Prime
for a being Element of (GF p) holds a |^ (n + 1) = (a |^ n) * a
let p be Prime; :: thesis: for a being Element of (GF p) holds a |^ (n + 1) = (a |^ n) * a
let a be Element of (GF p); :: thesis: a |^ (n + 1) = (a |^ n) * a
consider n1 being Nat such that
P1: a = n1 mod p by GF1;
a |^ n = (n1 |^ n) mod p by P1, EX4;
then (a |^ n) * a = ((n1 |^ n) * n1) mod p by P1, GF6
.= (n1 |^ (n + 1)) mod p by NEWTON:6 ;
hence a |^ (n + 1) = (a |^ n) * a by P1, EX4; :: thesis: verum