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

proof

let i be set ; :: thesis: ( i in SetPrimes implies ex j being set st S₁[i,j] )
assume i in SetPrimes ; :: thesis: ex j being set 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 set 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