deffunc H₁( Element of S) -> set = proj ((Carrier (A,$1)),i);
consider F being ManySortedSet of the carrier of S such that
A1: for s being Element of S holds F . s = H₁(s) from PBOOLE:sch 5();
F is ManySortedFunction of (product A),(A . i)

proof

let s be object ; :: according to PBOOLE:def 15 :: thesis: ( not s in the carrier of S or F . s is Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (A . i) . s))) )
assume A2: s in the carrier of S ; :: thesis: F . s is Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (A . i) . s)))
F . s is Function of ( the Sorts of (product A) . s),( the Sorts of (A . i) . s)

proof

reconsider s9 = s as Element of S by A2;
F . s = proj ((Carrier (A,s9)),i) by A1;
then reconsider F9 = F . s as Function ;
A3: rng F9 c= the Sorts of (A . i) . s

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F9 or y in the Sorts of (A . i) . s )
A4: ( dom (Carrier (A,s9)) = I & ex U0 being MSAlgebra over S st
( U0 = A . i & (Carrier (A,s9)) . i = the Sorts of U0 . s9 ) ) by PARTFUN1:def 2, PRALG_2:def 9;
assume y in rng F9 ; :: thesis: y in the Sorts of (A . i) . s
then y in rng (proj ((Carrier (A,s9)),i)) by A1;
then consider x1 being object such that
A5: x1 in dom (proj ((Carrier (A,s9)),i)) and
A6: y = (proj ((Carrier (A,s9)),i)) . x1 by FUNCT_1:def 3;
A7: x1 in product (Carrier (A,s9)) by A5;
then reconsider x1 = x1 as Function ;
y = x1 . i by A5, A6, CARD_3:def 16;
hence y in the Sorts of (A . i) . s by A7, A4, CARD_3:9; :: thesis: verum

end;

dom F9 = dom (proj ((Carrier (A,s9)),i)) by A1
.= product (Carrier (A,s9)) by CARD_3:def 16
.= the Sorts of (product A) . s by PRALG_2:def 10 ;
hence F . s is Function of ( the Sorts of (product A) . s),( the Sorts of (A . i) . s) by A2, A3, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

end;

hence F . s is Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (A . i) . s))) ; :: thesis: verum

end;

then reconsider F9 = F as ManySortedFunction of (product A),(A . i) ;
take F9 ; :: thesis: for s being Element of S holds F9 . s = proj ((Carrier (A,s)),i)
thus for s being Element of S holds F9 . s = proj ((Carrier (A,s)),i) by A1; :: thesis: verum