deffunc H₁( SortSymbol of S) -> set = product (Carrier (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 2, RELAT_1:def 18;
take f ; :: thesis: for s being SortSymbol of S holds f . s = product (Carrier (A,s))
thus for s being SortSymbol of S holds f . s = product (Carrier (A,s)) by A1; :: thesis: verum