let a be Nat; :: thesis:
let n be prime Nat; :: thesis:
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]

let k be Nat; :: thesis:
assume A0: S₁[k] ; :: thesis:
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:

end;