deffunc H₁( set ) -> set = f . I;
A1: for e being set st e in I holds
H₁(e) <> {} ;
consider g being ManySortedSet of I such that
W: for e being set st e in I holds
g . e in H₁(e) from PBOOLE:sch 1(A1);
g is f -compatible

proof

let x be set ; :: according to FUNCT_1:def 20 :: thesis: ( not x in proj1 g or g . x in f . x )
assume x in dom g ; :: thesis: g . x in f . x
then x in I by PARTFUN1:def 4;
hence g . x in f . x by W; :: thesis: verum

end;

then reconsider g = g as I -defined f -compatible Function ;
take g ; :: thesis: g is total
thus g is total ; :: thesis: verum