let n, a be Nat; :: thesis: ( n >= 1 implies PrimeDivisors (a |^ n) = PrimeDivisors a )
assume A0: n >= 1 ; :: thesis: PrimeDivisors (a |^ n) = PrimeDivisors a
thus PrimeDivisors (a |^ n) c= PrimeDivisors a :: according to XBOOLE_0:def 10 :: thesis: PrimeDivisors a c= PrimeDivisors (a |^ n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeDivisors (a |^ n) or x in PrimeDivisors a )
assume x in PrimeDivisors (a |^ n) ; :: thesis: x in PrimeDivisors a
then consider k being Prime such that
S1: ( k = x & k divides a |^ n ) ;
k divides a by S1, NAT_3:5;
hence x in PrimeDivisors a by S1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeDivisors a or x in PrimeDivisors (a |^ n) )
assume x in PrimeDivisors a ; :: thesis: x in PrimeDivisors (a |^ n)
then consider k being Prime such that
S1: ( k = x & k divides a ) ;
a = a |^ 1 ;
then a divides a |^ n by A0, NEWTON:89;
then k divides a |^ n by S1, NAT_D:4;
hence x in PrimeDivisors (a |^ n) by S1; :: thesis: verum