deffunc H₁( Element of S) -> Subset of (Class (CompClass E,(CComp $1))) = OSClass E,$1;
consider f being Function such that
A1: dom f = the carrier of S and
A2: for i being Element of S holds f . i = H₁(i) from FUNCT_1:sch 4();
reconsider f1 = f as ManySortedSet of by A1, PARTFUN1:def 4, RELAT_1:def 18;
set f2 = f1;
f1 is order-sorted

proof

let s1, s2 be Element of S; :: according to OSALG_1:def 18 :: thesis: ( not s1 <= s2 or f1 . s1 c= f1 . s2 )
assume A3: s1 <= s2 ; :: thesis: f1 . s1 c= f1 . s2
( f1 . s1 = OSClass E,s1 & f1 . s2 = OSClass E,s2 ) by A2;
hence f1 . s1 c= f1 . s2 by A3, Th11; :: thesis: verum

end;

hence ex b₁ being OrderSortedSet of st
for s1 being Element of S holds b₁ . s1 = OSClass E,s1 by A2; :: thesis: verum