theorem Th55: :: NAT_3:55

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