defpred S1[ object , object ] means \$2 = (F . \$1) | (C . \$1);
A1: for i being object st i in I holds
ex u being object st S1[i,u] ;
consider H being Function such that
A2: ( 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 i being object st i in I holds
H . i is Function of (C . i),(B . i)
proof
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;
per cases ( B . i is empty or not B . i is empty ) ;
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 ; :: thesis: verum
end;
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 ;
hence H . i is Function of (C . i),(B . i) by ; :: thesis: verum
end;
end;
end;
then reconsider H = H as ManySortedFunction of C,B by PBOOLE:def 15;
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