deffunc H_{1}( Element of S) -> Subset of (TS (DTConMSA X)) = FreeSort (X,$1);

consider f being Function such that

A1: ( dom f = the carrier of S & ( for d being Element 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;

take f ; :: thesis: for s being SortSymbol of S holds f . s = FreeSort (X,s)

thus for s being SortSymbol of S holds f . s = FreeSort (X,s) by A1; :: thesis: verum

consider f being Function such that

A1: ( dom f = the carrier of S & ( for d being Element 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;

take f ; :: thesis: for s being SortSymbol of S holds f . s = FreeSort (X,s)

thus for s being SortSymbol of S holds f . s = FreeSort (X,s) by A1; :: thesis: verum