theorem Th29: :: NAT_3:29

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