let n be non zero Nat; :: thesis: 0 in rng (pfexp n)
not SetPrimes c= support (pfexp n) ;
then consider p being object such that
A1: ( p in SetPrimes & not p in support (pfexp n) ) by TARSKI:def 3;
reconsider p = p as Prime by A1, NEWTON:def 6;
( dom (pfexp n) = SetPrimes & (pfexp n) . p = 0 ) by A1, PRE_POLY:def 7, PARTFUN1:def 2;
hence 0 in rng (pfexp n) by A1, FUNCT_1:def 3; :: thesis: verum