defpred S_{1}[ object , object ] means $2 = (F . $1) " ;

A3: for i being object st i in I holds

ex u being object st S_{1}[i,u]
;

consider H being Function such that

A4: ( dom H = I & ( for i being object st i in I holds

S_{1}[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 object st x in dom H holds

H . x is Function

for i being object st i in I holds

H . i is Function of (B . i),(A . i)

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

A3: for i being object st i in I holds

ex u being object st S

consider H being Function such that

A4: ( dom H = I & ( for i being object st i in I holds

S

reconsider H = H as ManySortedSet of I by A4, PARTFUN1:def 2, RELAT_1:def 18;

for x being object st x in dom H holds

H . x is Function

proof

then reconsider H = H as ManySortedFunction of I by FUNCOP_1:def 6;
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;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

for i being object st i in I holds

H . i is Function of (B . i),(A . i)

proof

then reconsider H = H as ManySortedFunction of B,A by PBOOLE:def 15;
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 A6, PARTFUN1:def 2;

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 A7, FUNCT_2:25;

hence H . i is Function of (B . i),(A . i) by A4, A6; :: thesis: verum

end;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;

rng f = B . i by A2, A6;

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

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