set f = PFactors 1;
for z being object st z in dom (PFactors 1) holds
(PFactors 1) . z = 0
proof
let z be object ; :: 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 2;
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 PRE_POLY:def 7; :: thesis: verum
end;
then A1: PFactors 1 = (dom (PFactors 1)) --> 0 by FUNCOP_1:11;
dom (PFactors 1) = SetPrimes by PARTFUN1:def 2;
hence PFactors 1 = EmptyBag SetPrimes by A1, PBOOLE:def 3; :: thesis: verum