deffunc H₁( set ) -> set = f | (A . $1);
consider F being ManySortedSet of I such that
A1: for i being set st i in I holds
F . i = H₁(i) from PBOOLE:sch 4();
F is Function-yielding

proof

let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 F or F . x is set )
assume x in dom F ; :: thesis: F . x is set
then x in I by PARTFUN1:def 2;
then F . x = f | (A . x) by A1;
hence F . x is set ; :: thesis: verum

end;

hence ex b₁ being ManySortedFunction of I st
for i being set st i in I holds
b₁ . i = f | (A . i) by A1; :: thesis: verum