deffunc H₁( Element of S) -> Element of bool [:( the Sorts of U1 . S),( the Sorts of U1 . S):] = id ( the Sorts of U1 . S);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;
for i being set st i in the carrier of S holds
f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)

proof

let i be set ; :: thesis: ( i in the carrier of S implies f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) )
assume i in the carrier of S ; :: thesis: f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
then f . i = id ( the Sorts of U1 . i) by A1;
hence f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) ; :: thesis: verum

end;

then reconsider f = f as ManySortedRelation of the Sorts of U1, the Sorts of U1 by MSUALG_4:def 1;
reconsider f = f as ManySortedRelation of U1 ;
set f1 = f;
A2: f is os-compatible

proof

reconsider X = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
let s1, s2 be Element of S; :: according to OSALG_4:def 1 :: thesis: ( s1 <= s2 implies for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 ) )
assume A3: s1 <= s2 ; :: thesis: for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 )
reconsider s3 = s1, s4 = s2 as Element of S ;
let x, y be set ; :: thesis: ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 implies ( [x,y] in f . s1 iff [x,y] in f . s2 ) )
assume that
A4: x in the Sorts of U1 . s1 and
y in the Sorts of U1 . s1 ; :: thesis: ( [x,y] in f . s1 iff [x,y] in f . s2 )
A5: f . s1 = id (X . s1) by A1;
A6: f . s2 = id (X . s2) by A1;
X . s3 c= X . s4 by A3, OSALG_1:def 16;
then id (X . s1) c= id (X . s2) by SYSREL:15;
hence ( [x,y] in f . s1 implies [x,y] in f . s2 ) by A5, A6; :: thesis: ( [x,y] in f . s2 implies [x,y] in f . s1 )
assume [x,y] in f . s2 ; :: thesis: [x,y] in f . s1
then x = y by A6, RELAT_1:def 10;
hence [x,y] in f . s1 by A5, A4, RELAT_1:def 10; :: thesis: verum

end;

take f ; :: thesis: ( f is OrderSortedRelation of U1 & f is MSEquivalence-like )
for i being object
for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)

proof

let i be object ; :: thesis: for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
let R be Relation of ( the Sorts of U1 . i); :: thesis: ( i in the carrier of S & f . i = R implies R is Equivalence_Relation of ( the Sorts of U1 . i) )
assume ( i in the carrier of S & f . i = R ) ; :: thesis: R is Equivalence_Relation of ( the Sorts of U1 . i)
then R = id ( the Sorts of U1 . i) by A1;
hence R is Equivalence_Relation of ( the Sorts of U1 . i) ; :: thesis: verum

end;

then f is MSEquivalence_Relation-like by MSUALG_4:def 2;
hence ( f is OrderSortedRelation of U1 & f is MSEquivalence-like ) by A2, Def2, MSUALG_4:def 3; :: thesis: verum