theorem Th18: :: NAT_4:18

for q1, q, n1 being Element of NAT st q1 divides q |^ n1 & q is prime & q1 is prime holds
q = q1