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, PBOOLE:def 3;
for x being set st x in dom f holds
f . x is Relation

proof

let x be set ; :: thesis:
assume x in dom f ; :: thesis:
then reconsider s = x as Element of S by A2;
f . s = MSCng F,s by A2;
hence f . x is Relation ; :: thesis:

end;

then reconsider f = f as ManySortedRelation of the carrier of S by Def1;
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:
assume i in the carrier of S ; :: thesis:
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:

end;

then reconsider f = f as ManySortedRelation of the Sorts of U1 by Def2;
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:
let R be Relation of the Sorts of U1 . i; :: thesis:
assume A3: ( i in the carrier of S & f . i = R ) ; :: thesis:
then reconsider s = i as Element of S ;
R = MSCng F,s by A2, A3;
hence R is Equivalence_Relation of the Sorts of U1 . i ; :: thesis:

end;

then f is MSEquivalence_Relation-like by Def3;
then reconsider f = f as MSEquivalence-like ManySortedRelation of U1 by Def5;
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:
let x, y be Element of Args o,U1; :: thesis:
assume A4: for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ; :: thesis:
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) & dom y = dom (the_arity_of o) & dom (F # x) = dom (the_arity_of o) & dom (F # y) = dom (the_arity_of o) ) by MSUALG_3:6;

now

let n be set ; :: thesis:
assume A6: n in dom (the_arity_of o) ; :: thesis:
then reconsider m = n as Nat by ORDINAL1:def 13;
A7: ( (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, MSUALG_3:def 8;
A8: (the_arity_of o) /. m = (the_arity_of o) . m by A6, PARTFUN1:def 8;
(the_arity_of o) . m in rng (the_arity_of o) by A6, FUNCT_1:def 5;
then reconsider s = (the_arity_of o) . m as SortSymbol of S ;
A9: n in dom (the Sorts of U1 * (the_arity_of o)) by A6, PBOOLE:def 3;
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 A9, FUNCT_1:22;
A10: [x1,y1] in f . ((the_arity_of o) /. m) by A4, A5, A6;
f . ((the_arity_of o) /. m) = MSCng F,s by A2, A8;
hence (F # x) . n = (F # y) . n by A7, A8, A10, Def19; :: thesis:

end;

then A11: F # x = F # y by A5, FUNCT_1:9;
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 PBOOLE:def 3;
reconsider ro = the_result_sort_of o as SortSymbol of S ;
A15: f . ro = MSCng F,ro by A2;
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 . ro by MSUALG_1:def 7 ;
then reconsider Dx = (Den o,U1) . x, Dy = (Den o,U1) . y as Element of the Sorts of U1 . ro ;
( (F . ro) . Dx = (Den o,U2) . (F # x) & (F . ro) . Dy = (Den o,U2) . (F # y) ) by A1, MSUALG_3:def 9;
hence [((Den o,U1) . x),((Den o,U1) . y)] in f . (the_result_sort_of o) by A11, A15, Def19; :: thesis:

end;

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