deffunc H₁( Element of S1) -> set = meet (OSSubSort (A,$1));
consider f being Function such that
A1: ( dom f = the carrier of S1 & ( for s being Element of S1 holds f . s = H₁(s) ) ) 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

reconsider u0 = the Sorts of OU0 as MSSubset of OU0 by PBOOLE:def 18;
let x be object ; :: according to PBOOLE:def 2 :: thesis: ( not x in the carrier of S1 or f . x c= the Sorts of OU0 . x )
assume x in the carrier of S1 ; :: thesis: f . x c= the Sorts of OU0 . x
then reconsider s = x as SortSymbol of S1 ;
A2: f . s = meet (OSSubSort (A,s)) by A1;
u0 is OrderSortedSet of S1 by OSALG_1:17;
then A3: u0 is OSSubset of OU0 by Def2;
u0 in OSSubSort A by Th17;
then the Sorts of OU0 . s in OSSubSort (A,s) by A3, Def10;
hence f . x c= the Sorts of OU0 . x by A2, SETFAM_1:3; :: 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 = meet (OSSubSort (A,s)) ) )
reconsider f1 = f as ManySortedSet of S1 ;
for s1, s2 being Element of S1 st s1 <= s2 holds
f1 . s1 c= f1 . s2

proof

let s1, s2 be Element of S1; :: thesis: ( s1 <= s2 implies f1 . s1 c= f1 . s2 )
assume s1 <= s2 ; :: thesis: f1 . s1 c= f1 . s2
then A4: meet (OSSubSort (A,s1)) c= meet (OSSubSort (A,s2)) by Th21, SETFAM_1:14;
f1 . s1 = meet (OSSubSort (A,s1)) by A1;
hence f1 . s1 c= f1 . s2 by A1, A4; :: thesis: verum

end;

then f is OrderSortedSet of S1 by OSALG_1:def 16;
hence ( f is OSSubset of OU0 & ( for s being SortSymbol of S1 holds f . s = meet (OSSubSort (A,s)) ) ) by A1, Def2; :: thesis: verum