let p be Prime; :: thesis: for n being non zero Nat holds (ppf (p |^ n)) . p = p |^ n
let n be non zero Nat; :: thesis: (ppf (p |^ n)) . p = p |^ n
p > 1 by INT_2:def 4;
then p |-count (p |^ n) = n by Th25;
hence (ppf (p |^ n)) . p = p |^ n by Th56; :: thesis: verum