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

proof

let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I or X . i is Element of bool [:(A . i),(B . i):] )
assume A2: i in I ; :: thesis: X . i is Element of bool [:(A . i),(B . i):]
then reconsider Bi = B . i as non empty set ;
A3: X . i = pr1 (F . i) by A1, A2;
then reconsider Xi = X . i as Function ;
A4: F . i is Function of (A . i),([|B,C|] . i) by A2, PBOOLE:def 15;
A5: rng Xi c= Bi

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in rng Xi or q in Bi )
assume q in rng Xi ; :: thesis: q in Bi
then consider x being object such that
A6: x in dom Xi and
A7: Xi . x = q by FUNCT_1:def 3;
x in dom (F . i) by A3, A6, MCART_1:def 12;
then A8: ( Xi . x = ((F . i) . x) `1 & (F . i) . x in rng (F . i) ) by A3, FUNCT_1:def 3, MCART_1:def 12;
rng (F . i) c= [|B,C|] . i by A4, RELAT_1:def 19;
then A9: rng (F . i) c= [:(B . i),(C . i):] by A2, PBOOLE:def 16;
assume not q in Bi ; :: thesis: contradiction
hence contradiction by A7, A9, A8, MCART_1:10; :: thesis: verum

end;

dom (F . i) = A . i by A2, A4, FUNCT_2:def 1;
then dom Xi = A . i by A3, MCART_1:def 12;
hence X . i is Element of bool [:(A . i),(B . i):] by A5, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

end;

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