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

A1: for i being object st i in I holds

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

consider H being Function such that

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

S_{1}[i,H . i] ) )
from CLASSES1:sch 1(A1);

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

for i being object st i in I holds

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

take H ; :: thesis: for i being set st i in I holds

H . i = (F . i) | (C . i)

thus for i being set st i in I holds

H . i = (F . i) | (C . i) by A2; :: thesis: verum

A1: for i being object st i in I holds

ex u being object st S

consider H being Function such that

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

S

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

for i being object st i in I holds

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

proof

then reconsider H = H as ManySortedFunction of C,B by PBOOLE:def 15;
let i be object ; :: thesis: ( i in I implies H . i is Function of (C . i),(B . i) )

assume A3: i in I ; :: thesis: H . i is Function of (C . i),(B . i)

then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;

A4: H . i = f | (C . i) by A2, A3;

C c= A by PBOOLE:def 18;

then A5: C . i c= A . i by A3;

end;assume A3: i in I ; :: thesis: H . i is Function of (C . i),(B . i)

then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;

A4: H . i = f | (C . i) by A2, A3;

C c= A by PBOOLE:def 18;

then A5: C . i c= A . i by A3;

per cases
( B . i is empty or not B . i is empty )
;

end;

suppose A6:
B . i is empty
; :: thesis: H . i is Function of (C . i),(B . i)

then
H . i = {}
by A4;

hence H . i is Function of (C . i),(B . i) by A6, FUNCT_2:def 1, RELSET_1:12; :: thesis: verum

end;hence H . i is Function of (C . i),(B . i) by A6, FUNCT_2:def 1, RELSET_1:12; :: thesis: verum

suppose A8:
not B . i is empty
; :: thesis: H . i is Function of (C . i),(B . i)

then A9:
dom f = A . i
by FUNCT_2:def 1;

A10: rng (f | (C . i)) c= B . i by RELAT_1:def 19;

dom (f | (C . i)) = (dom f) /\ (C . i) by RELAT_1:61

.= C . i by A5, A9, XBOOLE_1:28 ;

hence H . i is Function of (C . i),(B . i) by A4, A8, A10, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

end;A10: rng (f | (C . i)) c= B . i by RELAT_1:def 19;

dom (f | (C . i)) = (dom f) /\ (C . i) by RELAT_1:61

.= C . i by A5, A9, XBOOLE_1:28 ;

hence H . i is Function of (C . i),(B . i) by A4, A8, A10, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

take H ; :: thesis: for i being set st i in I holds

H . i = (F . i) | (C . i)

thus for i being set st i in I holds

H . i = (F . i) | (C . i) by A2; :: thesis: verum