defpred S₁[ set , set ] means $2 is Element of B . $1;
A1: for i being set st i in I holds
ex j being set st S₁[i,j]

proof

let i be set ; :: thesis: ( i in I implies ex j being set st S₁[i,j] )
assume i in I ; :: thesis: ex j being set st S₁[i,j]
consider j being Element of B . i;
reconsider j = j as set ;
take j ; :: thesis: S₁[i,j]
thus S₁[i,j] ; :: thesis: verum

end;

thus ex f being ManySortedSet of I st
for i being set st i in I holds
S₁[i,f . i] from PBOOLE:sch 3(A1); :: thesis: verum