defpred S1[ object , object ] means \$2 = (F . \$1) " ;
A3: for i being object st i in I holds
ex u being object st S1[i,u] ;
consider H being Function such that
A4: ( dom H = I & ( for i being object st i in I holds
S1[i,H . i] ) ) from reconsider H = H as ManySortedSet of I by ;
for x being object st x in dom H holds
H . x is Function
proof
let x be object ; :: 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 object st i in I holds
H . i is Function of (B . i),(A . i)
proof
let i be object ; :: 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 ;
then A7: f is one-to-one by A1;
rng f = B . i by A2, A6;
then f " is Function of (B . i),(A . i) by ;
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