set f = pfexp n;
let x be set ; :: according to VALUED_0:def 12 :: thesis: ( not x in dom (pfexp n) or (pfexp n) . x is natural )
assume x in dom (pfexp n) ; :: thesis: (pfexp n) . x is natural
then reconsider x = x as Prime by Th33;
(pfexp n) . x = x |-count n by Def8;
hence (pfexp n) . x is natural ; :: thesis: verum