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

proof

let z be object ; :: thesis: ( z in dom (Bnumber_of_divisors 1) implies (Bnumber_of_divisors 1) . z = 0 )
assume z in dom (Bnumber_of_divisors 1) ; :: thesis: (Bnumber_of_divisors 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 (Bnumber_of_divisors 1) by BDef;
hence (Bnumber_of_divisors 1) . z = 0 by PRE_POLY:def 7; :: thesis: verum

end;

then A1: Bnumber_of_divisors 1 = (dom (Bnumber_of_divisors 1)) --> 0 by FUNCOP_1:11;
dom (Bnumber_of_divisors 1) = SetPrimes by PARTFUN1:def 2;
hence Bnumber_of_divisors 1 = EmptyBag SetPrimes by A1, PBOOLE:def 3; :: thesis: verum