let p be Prime; :: thesis: for n being non empty natural number holds (ppf (p |^ n)) . p = p |^ n
let n be non empty natural number ; :: 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