deffunc H₁( Nat) -> Element of NAT = $1 |-count n;
defpred S₁[ object , object ] means ex w being Nat st
( w = $1 & $2 = H₁(w) );
A1: for i being object st i in SetPrimes holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in SetPrimes implies ex j being object st S₁[i,j] )
assume i in SetPrimes ; :: thesis: ex j being object st S₁[i,j]
then reconsider i = i as prime Element of NAT by NEWTON:def 6;
take H₁(i) ; :: thesis: S₁[i,H₁(i)]
take i ; :: thesis: ( i = i & H₁(i) = H₁(i) )
thus ( i = i & H₁(i) = H₁(i) ) ; :: thesis: verum

end;

consider f being ManySortedSet of SetPrimes such that
A2: for i being object st i in SetPrimes holds
S₁[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 S₁[i,f . i] by A2;
hence f . i = i |-count n ; :: thesis: verum