A1: rng (PFactors n) c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (PFactors n) or x in NAT )
assume x in rng (PFactors n) ; :: thesis: x in NAT
then consider y being object such that
A2: y in dom (PFactors n) and
A3: (PFactors n) . y = x by FUNCT_1:def 3;
A4: y in SetPrimes by A2, PARTFUN1:def 2;

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

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

then x = y by A3, Def6;
hence x in NAT by A4; :: thesis: verum

end;

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

then not y in support (PFactors n) by Def6;
then x = 0 by A3, PRE_POLY:def 7;
hence x in NAT ; :: thesis: verum

end;

end;

end;

support (PFactors n) = support (pfexp n) by Def6;
hence ( PFactors n is finite-support & PFactors n is natural-valued ) by A1, PRE_POLY:def 8, VALUED_0:def 6; :: thesis: verum