theorem Th32: :: NAT_3:32

for b being Nat
for p being Prime
for a being non zero Nat holds p |-count (a |^ b) = b * (p |-count a)