deffunc H₁( object ) -> set = pr2 (F . $1);
consider X being ManySortedSet of I such that
A13: for i being object st i in I holds
X . i = H₁(i) from PBOOLE:sch 4();
X is ManySortedFunction of A,C

proof

let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I or X . i is Element of bool [:(A . i),(C . i):] )
assume A14: i in I ; :: thesis: X . i is Element of bool [:(A . i),(C . i):]
then reconsider Ci = C . i as non empty set ;
A15: X . i = pr2 (F . i) by A13, A14;
then reconsider Xi = X . i as Function ;
A16: F . i is Function of (A . i),([|B,C|] . i) by A14, PBOOLE:def 15;
A17: rng Xi c= Ci

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in rng Xi or q in Ci )
assume q in rng Xi ; :: thesis: q in Ci
then consider x being object such that
A18: x in dom Xi and
A19: Xi . x = q by FUNCT_1:def 3;
x in dom (F . i) by A15, A18, MCART_1:def 13;
then A20: ( Xi . x = ((F . i) . x) `2 & (F . i) . x in rng (F . i) ) by A15, FUNCT_1:def 3, MCART_1:def 13;
rng (F . i) c= [|B,C|] . i by A16, RELAT_1:def 19;
then A21: rng (F . i) c= [:(B . i),(C . i):] by A14, PBOOLE:def 16;
assume not q in Ci ; :: thesis: contradiction
hence contradiction by A19, A21, A20, MCART_1:10; :: thesis: verum

end;

dom (F . i) = A . i by A14, A16, FUNCT_2:def 1;
then dom Xi = A . i by A15, MCART_1:def 13;
hence X . i is Element of bool [:(A . i),(C . i):] by A17, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

end;

then reconsider X = X as ManySortedFunction of A,C ;
take X ; :: thesis: for i being set st i in I holds
X . i = pr2 (F . i)
thus for i being set st i in I holds
X . i = pr2 (F . i) by A13; :: thesis: verum