theorem Th28: :: NAT_3:28

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