let k be Nat; :: thesis: for p being Prime st k >= 1 holds
PrimeDivisors (p |^ k) = {p}
let p be Prime; :: thesis: ( k >= 1 implies PrimeDivisors (p |^ k) = {p} )
assume A0: k >= 1 ; :: thesis: PrimeDivisors (p |^ k) = {p}
defpred S₁[ Nat] means PrimeDivisors (p |^ ($1 + 1)) = {p};
A1: S₁[ 0 ] by LemmaOne;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
PrimeDivisors (p |^ ((k + 1) + 1)) = PrimeDivisors ((p |^ (k + 1)) * p) by NEWTON:6
.= (PrimeDivisors (p |^ (k + 1))) \/ (PrimeDivisors p) by DivisorsMulti
.= (PrimeDivisors (p |^ (k + 1))) \/ {p} by LemmaOne
.= {p} by A3 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
then S₁[k -' 1] ;
hence PrimeDivisors (p |^ k) = {p} by A0, XREAL_1:235; :: thesis: verum