let a, n be Nat; :: thesis: ( a |^ n is prime implies n = 1 )
set p = a |^ n;
assume that
A1: a |^ n > 1 and
A2: for n being Nat holds
( not n divides a |^ n or n = 1 or n = a |^ n ) ; :: according to INT_2:def 4 :: thesis: n = 1

per cases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6;

suppose n = 0 ; :: thesis: n = 1

hence n = 1 by A1, NEWTON:4; :: thesis: verum

end;

suppose ex k being Nat st n = k + 1 ; :: thesis: n = 1

then consider k being Nat such that
A3: n = k + 1 ;
A4: a |^ n = (a |^ k) * a by A3, NEWTON:6;
A5: k in NAT by ORDINAL1:def 12;
a divides (a |^ k) * a ;

per cases then ( a = 1 or a = a |^ n ) by A2, A4;

suppose a = 1 ; :: thesis: n = 1

hence n = 1 by A1; :: thesis: verum

end;

suppose a = a |^ n ; :: thesis: n = 1

then 1 * a = (a |^ k) * a by A3, NEWTON:6;
then k = 0 by A1, A4, A5, WEDDWITT:1, XCMPLX_1:5;
hence n = 1 by A3; :: thesis: verum

end;

end;

end;

end;