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

proof

let i be object ; :: thesis: ( i in I implies ex j being object st S₁[i,j] )
assume i in I ; :: thesis: ex j being object st S₁[i,j]
set j = the Element of B . i;
reconsider j = the Element of B . i 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 object st i in I holds
S₁[i,f . i] from PBOOLE:sch 3(A1); :: thesis: verum