deffunc H₁( 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₁(d) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of by A1, PARTFUN1:def 4, 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