let a be Nat; :: 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);
( p > 1 & (pfexp (p |^ a)) . p = p |-count (p |^ a) ) by Def8, INT_2:def 4;
hence (pfexp (p |^ a)) . p = a by Th25; :: thesis: verum