theorem NAT332: :: NEWTON03:78

for a being prime Nat
for b being non zero Integer
for c being Nat holds a |-count (b |^ c) = c * (a |-count b)