deffunc H₁( SortSymbol of S) -> Subset of (the Sorts of U0 . $1) = Constants U0,$1;
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being SortSymbol of S holds f . d = H₁(d) ) ) 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

let s be set ; :: according to PBOOLE:def 5 :: thesis: ( not s in the carrier of S or f . s c= the Sorts of U0 . s )
assume s in the carrier of S ; :: thesis: f . s c= the Sorts of U0 . s
then reconsider s1 = s as SortSymbol of S ;
f . s1 = Constants U0,s1 by A1;
hence f . s c= the Sorts of U0 . s ; :: 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 = Constants U0,s
thus for s being SortSymbol of S holds f . s = Constants U0,s by A1; :: thesis: verum