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

proof

let x be object ; :: according to FUNCT_1:def 14 :: thesis: ( not x in dom 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 2;
hence g . x in f . x by A2; :: 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