let p be Prime; :: according to INT_7:def 1 :: thesis: ( p in support (ppf n) implies ex n being natural number st
( 0 < n & (ppf n) . p = p |^ n ) )
assume A1: p in support (ppf n) ; :: thesis: ex n being natural number 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 k = p |-count n; :: thesis: ( 0 < k & (ppf n) . p = p |^ k )
p in support (pfexp n) by A1, NAT_3:def 9;
hence ( 0 < k & (ppf n) . p = p |^ k ) by A2, NAT_3:def 9; :: thesis: verum