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

proof

let z be object ; :: thesis: ( z in dom (pfexp 1) implies (pfexp 1) . z = 0 )
assume z in dom (pfexp 1) ; :: thesis: (pfexp 1) . z = 0
then reconsider z = z as Prime by Th33;
A1: z <> 1 by INT_2:def 4;
(pfexp 1) . z = z |-count 1 by Def8
.= 0 by A1, Th21 ;
hence (pfexp 1) . z = 0 ; :: thesis: verum

end;

then A2: pfexp 1 = (dom (pfexp 1)) --> 0 by FUNCOP_1:11;
dom (pfexp 1) = SetPrimes by PARTFUN1:def 2;
hence pfexp 1 = EmptyBag SetPrimes by A2; :: thesis: verum