let a, k be Nat; :: thesis: for p being odd Prime st p divides a + 1 holds
( p |^ (k + 1) divides (a |^ (p |^ k)) + 1 & p |^ k divides (a |^ (p |^ k)) + 1 )
let p be odd Prime; :: thesis: ( p divides a + 1 implies ( p |^ (k + 1) divides (a |^ (p |^ k)) + 1 & p |^ k divides (a |^ (p |^ k)) + 1 ) )
assume A1: p divides a + 1 ; :: thesis: ( p |^ (k + 1) divides (a |^ (p |^ k)) + 1 & p |^ k divides (a |^ (p |^ k)) + 1 )
defpred S₁[ Nat] means p |^ ($1 + 1) divides (a |^ (p |^ $1)) + 1;
p |^ 0 = 1 by NEWTON:4;
then A2: S₁[ 0 ] by A1;
A3: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

let x be Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
assume S₁[x] ; :: thesis: S₁[x + 1]
then p |^ (x + 2) divides (a |^ (p |^ (x + 1))) + 1 by Th22;
hence S₁[x + 1] ; :: thesis: verum

end;

for x being Nat holds S₁[x] from NAT_1:sch 2(A2, A3);
hence A4: p |^ (k + 1) divides (a |^ (p |^ k)) + 1 ; :: thesis: p |^ k divides (a |^ (p |^ k)) + 1
p |^ k divides p |^ (k + 1) by NEWTON:89, NAT_1:11;
hence p |^ k divides (a |^ (p |^ k)) + 1 by A4, NAT_D:4; :: thesis: verum