let p be Prime; :: according to INT_7:def 1 :: thesis: ( p in support (ppf n) implies ex n being Nat st
( 0 < n & (ppf n) . p = p |^ n ) )
assume A1: p in support (ppf n) ; :: thesis: ex n being Nat st
( 0 < n & (ppf n) . p = p |^ n )
A2: p |-count n <> 0

proof

assume p |-count n = 0 ; :: thesis: contradiction
then (ppf n) . p = 0 by NAT_3:55;
hence contradiction by A1, PRE_POLY:def 7; :: thesis: verum

end;

take p |-count n ; :: thesis: ( 0 < p |-count n & (ppf n) . p = p |^ (p |-count n) )
p in support (pfexp n) by A1, NAT_3:def 9;
hence ( 0 < p |-count n & (ppf n) . p = p |^ (p |-count n) ) by A2, NAT_3:def 9; :: thesis: verum