let a be Nat; :: thesis: for n being prime Nat holds n divides (a |^ n) - a
let n be prime Nat; :: thesis: n divides (a |^ n) - a
defpred S₁[ Nat] means n divides ($1 |^ n) - $1;
L1: S₁[ 0 ] by INT_2:12;
L2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A0: S₁[k] ; :: thesis: S₁[k + 1]
n * k divides ((k + 1) |^ n) - ((k |^ n) + 1) by Th56;
then n divides ((k + 1) |^ n) - ((k |^ n) + 1) by INT_2:2, INT_1:def 3;
then n divides ((k |^ n) - k) + (((k + 1) |^ n) - ((k |^ n) + 1)) by A0, WSIERP_1:4;
hence S₁[k + 1] ; :: thesis: verum

end;

for x being Nat holds S₁[x] from NAT_1:sch 2(L1, L2);
hence n divides (a |^ n) - a ; :: thesis: verum