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 by A1, PARTFUN1:def 4, RELAT_1:def 18;
for x being set st x in dom f holds
f . x is Relation

proof

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

end;

then reconsider f = f as ManySortedRelation of by MSUALG_4:def 1;
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 2;
reconsider f = f as ManySortedRelation of U1 ;
for i being set
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 set ; :: 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 3;
then reconsider f = f as MSEquivalence-like ManySortedRelation of U1 by MSUALG_4:def 5;
set f1 = f;
f is os-compatible

proof

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 A2: 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 ;
reconsider X = the Sorts of U1 as OrderSortedSet of by OSALG_1:17;
X . s3 c= X . s4 by A2, OSALG_1:def 18;
then A3: id (X . s1) c= id (X . s2) by SYSREL:33;
A4: ( f . s1 = id (X . s1) & f . s2 = id (X . s2) ) by A1;
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 A5: ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 ) ; :: thesis: ( [x,y] in f . s1 iff [x,y] in f . s2 )
thus ( [x,y] in f . s1 implies [x,y] in f . s2 ) by A3, A4; :: 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 A4, RELAT_1:def 10;
hence [x,y] in f . s1 by A4, A5, RELAT_1:def 10; :: thesis: verum

end;

then reconsider f = f as MSEquivalence-like OrderSortedRelation of U1 by Def3;
take f ; :: thesis: f is MSCongruence-like
for o being Element of the carrier' of S
for x, y being Element of Args o,U1 st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) holds
[((Den o,U1) . x),((Den o,U1) . y)] in f . (the_result_sort_of o)

proof

let o be Element of the carrier' of S; :: thesis: for x, y being Element of Args o,U1 st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) holds
[((Den o,U1) . x),((Den o,U1) . y)] in f . (the_result_sort_of o)
let x, y be Element of Args o,U1; :: thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) implies [((Den o,U1) . x),((Den o,U1) . y)] in f . (the_result_sort_of o) )
assume A6: for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ; :: thesis: [((Den o,U1) . x),((Den o,U1) . y)] in f . (the_result_sort_of o)
A7: ( dom x = dom (the_arity_of o) & dom y = dom (the_arity_of o) ) by MSUALG_3:6;
for a being set st a in dom (the_arity_of o) holds
x . a = y . a

proof

let a be set ; :: thesis: ( a in dom (the_arity_of o) implies x . a = y . a )
assume A8: a in dom (the_arity_of o) ; :: thesis: x . a = y . a
then reconsider n = a as Nat ;
A9: (the_arity_of o) /. n = (the_arity_of o) . n by A8, PARTFUN1:def 8;
set ao = the_arity_of o;
(the_arity_of o) . n in rng (the_arity_of o) by A8, FUNCT_1:def 5;
then A10: f . ((the_arity_of o) . n) = id (the Sorts of U1 . ((the_arity_of o) . n)) by A1;
[(x . n),(y . n)] in f . ((the_arity_of o) . n) by A6, A7, A8, A9;
hence x . a = y . a by A10, RELAT_1:def 10; :: thesis: verum

end;

then A11: (Den o,U1) . x = (Den o,U1) . y by A7, FUNCT_1:9;
set r = the_result_sort_of o;
A12: f . (the_result_sort_of o) = id (the Sorts of U1 . (the_result_sort_of o)) by A1;
A13: ( dom the ResultSort of S = the carrier' of S & rng the ResultSort of S c= the carrier of S ) by FUNCT_2:def 1;
then A14: dom (the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def 4;
Result o,U1 = (the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def 10
.= the Sorts of U1 . (the ResultSort of S . o) by A13, A14, FUNCT_1:22
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def 7 ;
hence [((Den o,U1) . x),((Den o,U1) . y)] in f . (the_result_sort_of o) by A11, A12, RELAT_1:def 10; :: thesis: verum

end;

hence f is MSCongruence-like by MSUALG_4:def 6; :: thesis: verum