theorem Th19: :: NAT_5:19

for n, p being Nat st p is prime holds
NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n }