theorem Th56: :: NAT_3:56

for p being Prime
for n being non zero Nat st p |-count n <> 0 holds
(ppf n) . p = p |^ (p |-count n)