set f = PFactors 1;
for z being set st z in dom (PFactors 1) holds
(PFactors 1) . z = 0

proof

let z be set ; :: thesis: ( z in dom (PFactors 1) implies (PFactors 1) . z = 0 )
assume z in dom (PFactors 1) ; :: thesis: (PFactors 1) . z = 0
then z in SetPrimes by PARTFUN1:def 4;
then reconsider z = z as Element of NAT ;
support (pfexp 1) = {} ;
then not z in support (PFactors 1) by Def6;
hence (PFactors 1) . z = 0 by POLYNOM1:def 7; :: thesis: verum

end;

then A1: PFactors 1 = (dom (PFactors 1)) --> 0 by FUNCOP_1:17;
dom (PFactors 1) = SetPrimes by PARTFUN1:def 4;
hence PFactors 1 = EmptyBag SetPrimes by A1, POLYNOM1:def 15; :: thesis: verum