rng (ppf n) c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (ppf n) or y in NAT )
assume y in rng (ppf n) ; :: thesis: y in NAT
then consider x being object such that
A1: x in dom (ppf n) and
A2: (ppf n) . x = y by FUNCT_1:def 3;
dom (ppf n) = SetPrimes by PARTFUN1:def 2;
then reconsider x = x as prime Element of NAT by A1, NEWTON:def 6;

per cases ( x in support (pfexp n) or not x in support (pfexp n) ) ;

suppose x in support (pfexp n) ; :: thesis: y in NAT

then (ppf n) . x = x |^ (x |-count n) by Def9;
hence y in NAT by A2; :: thesis: verum

end;

suppose not x in support (pfexp n) ; :: thesis: y in NAT

then not x in support (ppf n) by Def9;
then (ppf n) . x = 0 by PRE_POLY:def 7;
hence y in NAT by A2; :: thesis: verum

end;

end;

end;

hence ppf n is natural-valued ; :: thesis: ppf n is finite-support
support (ppf n) = support (pfexp n) by Def9;
hence support (ppf n) is finite ; :: according to PRE_POLY:def 8 :: thesis: verum