deffunc H1( Nat) -> Element of NAT = $1 |-count n;
defpred S1[ object , object ] means ex w being Nat st
( w = $1 & $2 = H1(w) );
A1: for i being object st i in SetPrimes holds
ex j being object st S1[i,j]
proof
let i be object ; :: thesis: ( i in SetPrimes implies ex j being object st S1[i,j] )
assume i in SetPrimes ; :: thesis: ex j being object st S1[i,j]
then reconsider i = i as prime Element of NAT by NEWTON:def 6;
take H1(i) ; :: thesis: S1[i,H1(i)]
take i ; :: thesis: ( i = i & H1(i) = H1(i) )
thus ( i = i & H1(i) = H1(i) ) ; :: thesis: verum
end;
consider f being ManySortedSet of SetPrimes such that
A2: for i being object st i in SetPrimes holds
S1[i,f . i] from PBOOLE:sch 3(A1);
 take f ; :: thesis: for p being Prime holds f . p = p |-count n
let i be Prime; :: thesis: f . i = i |-count n
i in SetPrimes by NEWTON:def 6;
then S1[i,f . i] by A2;
hence f . i = i |-count n ; :: thesis: verum