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