let p be Prime; :: thesis: for n being non zero Nat st p |-count n <> 0 holds
(ppf n) . p = p |^ (p |-count n)
let n be non zero Nat; :: thesis: ( p |-count n <> 0 implies (ppf n) . p = p |^ (p |-count n) )
assume p |-count n <> 0 ; :: thesis: (ppf n) . p = p |^ (p |-count n)
then (pfexp n) . p <> 0 by Def8;
then p in support (pfexp n) by PRE_POLY:def 7;
hence (ppf n) . p = p |^ (p |-count n) by Def9; :: thesis: verum