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 the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;
set f2 = f1;
f1 is order-sorted

proof

let s1, s2 be Element of S; :: according to OSALG_1:def 16 :: 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, Th10; :: thesis: verum

end;

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