deffunc H₁( Element of S) -> Equivalence_Relation of ( the Sorts of U1 . $1) = MSCng (F,$1);
consider f being Function such that
A2: ( 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 A2, 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 reconsider s = i as Element of S ;
f . i = MSCng (F,s) by A2;
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 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 that
A3: i in the carrier of S and
A4: f . i = R ; :: thesis: R is Equivalence_Relation of ( the Sorts of U1 . i)
reconsider s = i as Element of S by A3;
R = MSCng (F,s) by A2, A4;
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;
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

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) )
set ao = the_arity_of o;
set ro = the_result_sort_of o;
set S1 = the Sorts of U1;
A5: dom x = dom (the_arity_of o) by MSUALG_3:6;
A6: dom y = dom (the_arity_of o) by MSUALG_3:6;
assume A7: 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)

A8: now :: thesis: for n being object st n in dom (the_arity_of o) holds
(F # x) . n = (F # y) . n

let n be object ; :: thesis: ( n in dom (the_arity_of o) implies (F # x) . n = (F # y) . n )
assume A9: n in dom (the_arity_of o) ; :: thesis: (F # x) . n = (F # y) . n
then reconsider m = n as Nat by ORDINAL1:def 12;
A10: ( (F # x) . m = (F . ((the_arity_of o) /. m)) . (x . m) & (F # y) . m = (F . ((the_arity_of o) /. m)) . (y . m) ) by A5, A6, A9, MSUALG_3:def 6;
(the_arity_of o) . m in rng (the_arity_of o) by A9, FUNCT_1:def 3;
then reconsider s = (the_arity_of o) . m as SortSymbol of S ;
A11: n in dom ( the Sorts of U1 * (the_arity_of o)) by A9, PARTFUN1:def 2;
then ( x . m in ( the Sorts of U1 * (the_arity_of o)) . n & y . m in ( the Sorts of U1 * (the_arity_of o)) . n ) by MSUALG_3:6;
then reconsider x1 = x . m, y1 = y . m as Element of the Sorts of U1 . s by A11, FUNCT_1:12;
A12: [x1,y1] in f . ((the_arity_of o) /. m) by A7, A5, A9;
A13: (the_arity_of o) /. m = (the_arity_of o) . m by A9, PARTFUN1:def 6;
then f . ((the_arity_of o) /. m) = MSCng (F,s) by A2;
hence (F # x) . n = (F # y) . n by A10, A13, A12, Def17; :: thesis: verum

end;

( dom (F # x) = dom (the_arity_of o) & dom (F # y) = dom (the_arity_of o) ) by MSUALG_3:6;
then A14: F # x = F # y by A8, FUNCT_1:2;
reconsider ro = the_result_sort_of o as SortSymbol of S ;
A15: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then A16: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def 2;
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 A15, A16, FUNCT_1:12
.= the Sorts of U1 . ro by MSUALG_1:def 2 ;
then reconsider Dx = (Den (o,U1)) . x, Dy = (Den (o,U1)) . y as Element of the Sorts of U1 . ro ;
A17: (F . ro) . Dy = (Den (o,U2)) . (F # y) by A1;
( f . ro = MSCng (F,ro) & (F . ro) . Dx = (Den (o,U2)) . (F # x) ) by A1, A2;
hence [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) by A14, A17, Def17; :: thesis: verum

end;

then reconsider f = f as MSCongruence of U1 by Def4;
take f ; :: thesis: for s being SortSymbol of S holds f . s = MSCng (F,s)
thus for s being SortSymbol of S holds f . s = MSCng (F,s) by A2; :: thesis: verum