let a be natural number ; :: thesis: for p being Prime holds (pfexp (p |^ a)) . p = a
let p be Prime; :: thesis: (pfexp (p |^ a)) . p = a
set f = pfexp (p |^ a);
A1: p > 1 by INT_2:def 5;
(pfexp (p |^ a)) . p = p |-count (p |^ a) by Def8;
hence (pfexp (p |^ a)) . p = a by A1, Th25; :: thesis: verum