deffunc H₁( Element of S) -> Element of K10(K11(( 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 Def1;
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 ;
then reconsider f = f as MSEquivalence-like ManySortedRelation of U1 by Def3;
take f ; :: thesis: f is MSCongruence-like
for o being OperSymbol 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

A2: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then A3: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def 2;
let o be OperSymbol 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) )
A4: dom x = dom (the_arity_of o) by MSUALG_3:6;
assume A5: 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)
A6: for a being object st a in dom (the_arity_of o) holds
x . a = y . a

proof

set ao = the_arity_of o;
let a be object ; :: thesis: ( a in dom (the_arity_of o) implies x . a = y . a )
assume A7: a in dom (the_arity_of o) ; :: thesis: x . a = y . a
then reconsider n = a as Nat by ORDINAL1:def 12;
(the_arity_of o) . n in rng (the_arity_of o) by A7, FUNCT_1:def 3;
then A8: f . ((the_arity_of o) . n) = id ( the Sorts of U1 . ((the_arity_of o) . n)) by A1;
(the_arity_of o) /. n = (the_arity_of o) . n by A7, PARTFUN1:def 6;
then [(x . n),(y . n)] in f . ((the_arity_of o) . n) by A5, A4, A7;
hence x . a = y . a by A8, RELAT_1:def 10; :: thesis: verum

end;

set r = the_result_sort_of o;
A9: f . (the_result_sort_of o) = id ( the Sorts of U1 . (the_result_sort_of o)) by A1;
A10: Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def 5
.= the Sorts of U1 . ( the ResultSort of S . o) by A2, A3, FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def 2 ;
dom y = dom (the_arity_of o) by MSUALG_3:6;
then (Den (o,U1)) . x = (Den (o,U1)) . y by A4, A6, FUNCT_1:2;
hence [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) by A9, A10, RELAT_1:def 10; :: thesis: verum

end;

hence f is MSCongruence-like ; :: thesis: verum