deffunc H_{1}( 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_{1}(d) ) )
from FUNCT_1:sch 4();

reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;

f c= the Sorts of U0

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

consider f being Function such that

A1: ( dom f = the carrier of S & ( for d being SortSymbol of S holds f . d = H

reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;

f c= the Sorts of U0

proof

then reconsider f = f as MSSubset of U0 by PBOOLE:def 18;
let s be object ; :: according to PBOOLE:def 2 :: 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;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

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