for p being Prime
for n being non zero Nat holds (PFactors (p |^ n)) * <*p*> = <*p*>