for p being Prime
for a being non zero Nat st p divides a holds
(pfexp a) . p <> 0