defpred S₁[ set , set ] means $2 = (F . $1) " ;
A3: for i being set st i in I holds
ex u being set st S₁[i,u] ;
consider H being Function such that
A4: ( dom H = I & ( for i being set st i in I holds
S₁[i,H . i] ) ) from CLASSES1:sch 1(A3);
reconsider H = H as ManySortedSet of I by A4, PARTFUN1:def 2, RELAT_1:def 18;
for x being set st x in dom H holds
H . x is Function

proof

let x be set ; :: thesis: ( x in dom H implies H . x is Function )
assume A5: x in dom H ; :: thesis: H . x is Function
then x in I by PARTFUN1:def 2;
then reconsider f = F . x as Function of (A . x),(B . x) by PBOOLE:def 15;
H . x = f " by A4, A5;
hence H . x is Function ; :: thesis: verum

end;

then reconsider H = H as ManySortedFunction of I by FUNCOP_1:def 6;
for i being set st i in I holds
H . i is Function of (B . i),(A . i)

proof

let i be set ; :: thesis: ( i in I implies H . i is Function of (B . i),(A . i) )
assume A6: i in I ; :: thesis: H . i is Function of (B . i),(A . i)
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
i in dom F by A6, PARTFUN1:def 2;
then A7: f is one-to-one by A1, Def2;
rng f = B . i by A2, A6, Def3;
then f " is Function of (B . i),(A . i) by A7, FUNCT_2:25;
hence H . i is Function of (B . i),(A . i) by A4, A6; :: thesis: verum

end;

then reconsider H = H as ManySortedFunction of B,A by PBOOLE:def 15;
take H ; :: thesis: for i being set st i in I holds
H . i = (F . i) "
thus for i being set st i in I holds
H . i = (F . i) " by A4; :: thesis: verum