deffunc H₁( Element of S1) -> set = union { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= $1 } ;
consider f being Function such that
A1: ( dom f = the carrier of S1 & ( for d being Element of S1 holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of the carrier of S1 by A1, PARTFUN1:def 2, RELAT_1:def 18;
f c= the Sorts of OU0

proof

let s be object ; :: according to PBOOLE:def 2 :: thesis: ( not s in the carrier of S1 or f . s c= the Sorts of OU0 . s )
assume s in the carrier of S1 ; :: thesis: f . s c= the Sorts of OU0 . s
then reconsider s1 = s as SortSymbol of S1 ;
f . s1 = OSConstants (OU0,s1) by A1;
hence f . s c= the Sorts of OU0 . s ; :: thesis: verum

end;

then reconsider f = f as MSSubset of OU0 by PBOOLE:def 18;
take f ; :: thesis: ( f is OSSubset of OU0 & ( for s being SortSymbol of S1 holds f . s = OSConstants (OU0,s) ) )
reconsider f1 = f as ManySortedSet of S1 ;
f1 is order-sorted

proof

let r1, r2 be Element of S1; :: according to OSALG_1:def 16 :: thesis: ( not r1 <= r2 or f1 . r1 c= f1 . r2 )
assume A2: r1 <= r2 ; :: thesis: f1 . r1 c= f1 . r2
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f1 . r1 or x in f1 . r2 )
assume x in f1 . r1 ; :: thesis: x in f1 . r2
then x in union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r1 } by A1;
then consider y being set such that
A3: ( x in y & y in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r1 } ) by TARSKI:def 4;
consider s3 being SortSymbol of S1 such that
A4: y = Constants (OU0,s3) and
A5: s3 <= r1 by A3;
s3 <= r2 by A2, A5, ORDERS_2:3;
then y in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r2 } by A4;
then x in union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r2 } by A3, TARSKI:def 4;
hence x in f1 . r2 by A1; :: thesis: verum

end;

hence f is OSSubset of OU0 by Def2; :: thesis: for s being SortSymbol of S1 holds f . s = OSConstants (OU0,s)
thus for s being SortSymbol of S1 holds f . s = OSConstants (OU0,s) by A1; :: thesis: verum