let a, n, k be Nat; :: thesis: ( k + 1 is prime implies k + 1 divides (a |^ ((n * k) + 1)) - a )
assume A1: k + 1 is prime ; :: thesis: k + 1 divides (a |^ ((n * k) + 1)) - a

per cases ( k + 1 divides a or not k + 1 divides a ) ;

suppose k + 1 divides a ; :: thesis: k + 1 divides (a |^ ((n * k) + 1)) - a

then k + 1 divides a * ((a |^ (n * k)) - 1) by INT_2:2;
then k + 1 divides (a * (a |^ (n * k))) - a ;
hence k + 1 divides (a |^ ((n * k) + 1)) - a by NEWTON:6; :: thesis: verum

end;

suppose not k + 1 divides a ; :: thesis: k + 1 divides (a |^ ((n * k) + 1)) - a

then B1: k + 1 divides (a |^ k) - 1 by A1, Th59;
(a |^ k) - (1 |^ k) divides ((a |^ k) |^ n) - ((1 |^ k) |^ n) by NEWTON01:33;
then k + 1 divides ((a |^ k) |^ n) - ((1 |^ k) |^ n) by B1, INT_2:9;
then k + 1 divides (a |^ (n * k)) - 1 by NEWTON:9;
then k + 1 divides a * ((a |^ (n * k)) - 1) by INT_2:2;
then k + 1 divides (a * (a |^ (n * k))) - a ;
hence k + 1 divides (a |^ ((n * k) + 1)) - a by NEWTON:6; :: thesis: verum

end;

end;