reconsider a = a as non zero square Element of NAT by INT_1:3;
|.p.| > 1 by NEWTON03:def 1;
then p |^ (p |-count a) divides a by NEWTON03:def 7;
then consider k being Nat such that
A0: a = (p |^ (p |-count a)) * k by NAT_D:def 3;
not p divides k by A0, NEWTON03:76;
then not k gcd p = p by INT_2:def 2;
then k,p are_coprime by PEPIN:2;
then A1: k,p |^ (p |-count a) are_coprime by WSIERP_1:10;
assume A2: not p |-count a is even ; :: thesis: contradiction
A3: not 2 -root (p |^ (p |-count a)) in NAT

proof

assume 2 -root (p |^ (p |-count a)) in NAT ; :: thesis: contradiction
then (2 -root (p |^ (p |-count a))) |^ 2 is square Nat ;
hence contradiction by A2; :: thesis: verum

end;

for c being Nat holds not k * (p |^ (p |-count a)) = c ^2

proof

assume ex c being Nat st k * (p |^ (p |-count a)) = c ^2 ; :: thesis: contradiction
then consider c being Nat such that
B1: c ^2 = k * (p |^ (p |-count a)) ;
k * (p |^ (p |-count a)) = c |^ 2 by B1, NEWTON:81;
hence contradiction by NEWTON03:14, A1, A3; :: thesis: verum

end;

hence contradiction by A0, PYTHTRIP:def 3; :: thesis: verum