deffunc H₁( SortSymbol of S) -> set = meet (SubSort A,$1);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for s being SortSymbol of S holds f . s = H₁(s) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 4, RELAT_1:def 18;
f c= the Sorts of U0

proof

reconsider u0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 23;
let x be set ; :: according to PBOOLE:def 5 :: thesis: ( not x in the carrier of S or f . x c= the Sorts of U0 . x )
A2: ( A c= u0 & Constants U0 c= u0 ) by PBOOLE:def 23;
assume x in the carrier of S ; :: thesis: f . x c= the Sorts of U0 . x
then reconsider s = x as SortSymbol of S ;
u0 is opers_closed by Th4;
then u0 in SubSort A by A2, Th14;
then A3: the Sorts of U0 . s in SubSort A,s by Def14;
f . s = meet (SubSort A,s) by A1;
hence f . x c= the Sorts of U0 . x by A3, SETFAM_1:4; :: thesis: verum

end;

then reconsider f = f as MSSubset of U0 by PBOOLE:def 23;
take f ; :: thesis: for s being SortSymbol of S holds f . s = meet (SubSort A,s)
thus for s being SortSymbol of S holds f . s = meet (SubSort A,s) by A1; :: thesis: verum