let a, n be Nat; :: thesis: for p being prime Nat st p divides a holds
p divides a |^ (n + 1)
let p be prime Nat; :: thesis: ( p divides a implies p divides a |^ (n + 1) )
assume p divides a ; :: thesis: p divides a |^ (n + 1)
then p divides a * (a |^ n) by INT_2:2;
hence p divides a |^ (n + 1) by NEWTON:6; :: thesis: verum