defpred S₁[ set , set ] means for f being Function of A . $1,B . $1 st f = F . $1 holds
$2 = f | (C . $1);
A1: for i being set st i in I holds
ex u being set st S₁[i,u]

proof

let i be set ; :: thesis: ( i in I implies ex u being set st S₁[i,u] )
assume i in I ; :: thesis: ex u being set st S₁[i,u]
then reconsider f = F . i as Function of A . i,B . i by PBOOLE:def 18;
take f | (C . i) ; :: thesis: S₁[i,f | (C . i)]
thus S₁[i,f | (C . i)] ; :: thesis: verum

end;

consider H being Function such that
A2: ( dom H = I & ( for i being set st i in I holds
S₁[i,H . i] ) ) from CLASSES1:sch 1(A1);
reconsider H = H as ManySortedSet of I by A2, PARTFUN1:def 4, RELAT_1:def 18;
for i being set st i in I holds
H . i is Function of C . i,B . i

proof

let i be set ; :: 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 18;
A4: H . i = f | (C . i) by A2, A3;
C c= A by PBOOLE:def 23;
then A5: C . i c= A . i by A3, PBOOLE:def 5;

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 A7: H . i = {} by A4;

now

per cases ( C . i = {} or C . i <> {} ) ;

suppose C . i = {} ; :: thesis: H . i is Function of C . i,B . i

hence H . i is Function of C . i,B . i by A7, RELSET_1:25; :: thesis: verum

end;

suppose C . i <> {} ; :: thesis: H . i is Function of C . i,B . i

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

end;

end;

end;

hence H . i is Function of C . i,B . i ; :: thesis: verum
set h = f | (C . i);

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:90
.= 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:11; :: thesis: verum

end;

end;

end;

then reconsider H = H as ManySortedFunction of C,B by PBOOLE:def 18;
take H ; :: thesis: for i being set st i in I holds
for f being Function of A . i,B . i st f = F . i holds
H . i = f | (C . i)
thus for i being set st i in I holds
for f being Function of A . i,B . i st f = F . i holds
H . i = f | (C . i) by A2; :: thesis: verum