defpred S₁[ object , object ] means $2 is Function of (A . $1),(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 Function of (A . i),(B . i);
reconsider j = the Function of (A . i),(B . i) as set ;
take j ; :: thesis: S₁[i,j]
thus S₁[i,j] ; :: thesis: verum

end;

consider f being ManySortedSet of I such that
A2: for i being object st i in I holds
S₁[i,f . i] from PBOOLE:sch 3(A1);
f is Function-yielding

proof

let i be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not i in dom f or f . i is set )
assume i in dom f ; :: thesis: f . i is set
then i in I by PARTFUN1:def 2;
hence f . i is set by A2; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of I ;
take f ; :: thesis: for i being object st i in I holds
f . i is Function of (A . i),(B . i)
let i be object ; :: thesis: ( i in I implies f . i is Function of (A . i),(B . i) )
assume i in I ; :: thesis: f . i is Function of (A . i),(B . i)
hence f . i is Function of (A . i),(B . i) by A2; :: thesis: verum