let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S holds id the Sorts of A is MSCongruence of A
let A be non-empty MSAlgebra over S; :: thesis: id the Sorts of A is MSCongruence of A
set J = id the Sorts of A;
for i being set st i in the carrier of S holds
(id the Sorts of A) . i is Relation of ( the Sorts of A . i)
proof
let i be set ; :: thesis: ( i in the carrier of S implies (id the Sorts of A) . i is Relation of ( the Sorts of A . i) )
assume i in the carrier of S ; :: thesis: (id the Sorts of A) . i is Relation of ( the Sorts of A . i)
then (id the Sorts of A) . i = id ( the Sorts of A . i) by MSUALG_3:def 1;
hence (id the Sorts of A) . i is Relation of ( the Sorts of A . i) ; :: thesis: verum
end;
then reconsider J = id the Sorts of A as ManySortedRelation of the Sorts of A by MSUALG_4:def 1;
for i being set
for R being Relation of ( the Sorts of A . i) st i in the carrier of S & J . i = R holds
R is Equivalence_Relation of ( the Sorts of A . i)
proof
let i be set ; :: thesis: for R being Relation of ( the Sorts of A . i) st i in the carrier of S & J . i = R holds
R is Equivalence_Relation of ( the Sorts of A . i)

let R be Relation of ( the Sorts of A . i); :: thesis: ( i in the carrier of S & J . i = R implies R is Equivalence_Relation of ( the Sorts of A . i) )
assume that
A1: i in the carrier of S and
A2: J . i = R ; :: thesis: R is Equivalence_Relation of ( the Sorts of A . i)
J . i = id ( the Sorts of A . i) by ;
hence R is Equivalence_Relation of ( the Sorts of A . i) by A2; :: thesis: verum
end;
then reconsider J = J as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A by MSUALG_4:def 2;
reconsider J = J as ManySortedRelation of A ;
reconsider J = J as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;
for o being OperSymbol of S
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . (() /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in J .
proof
let o be OperSymbol of S; :: thesis: for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . (() /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in J .

let x, y be Element of Args (o,A); :: thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . (() /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in J . )

assume A3: for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . (() /. n) ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in J .
A4: dom y = dom () by MSUALG_3:6
.= Seg (len ()) by FINSEQ_1:def 3 ;
A5: dom x = dom () by MSUALG_3:6
.= Seg (len ()) by FINSEQ_1:def 3 ;
then reconsider x9 = x, y9 = y as FinSequence by ;
now :: thesis: for n being Nat st n in dom x holds
x9 . n = y9 . n
let n be Nat; :: thesis: ( n in dom x implies x9 . n = y9 . n )
assume A6: n in dom x ; :: thesis: x9 . n = y9 . n
J . (() /. n) = id ( the Sorts of A . (() /. n)) by MSUALG_3:def 1;
then [(x . n),(y . n)] in id ( the Sorts of A . (() /. n)) by A3, A6;
hence x9 . n = y9 . n by RELAT_1:def 10; :: thesis: verum
end;
then A7: x = y by ;
(Den (o,A)) . x in Result (o,A) ;
then A8: (Den (o,A)) . x in ( the Sorts of A * the ResultSort of S) . o by MSUALG_1:def 5;
o in the carrier' of S ;
then o in dom the ResultSort of S by FUNCT_2:def 1;
then (Den (o,A)) . x in the Sorts of A . ( the ResultSort of S . o) by ;
then A9: (Den (o,A)) . x in the Sorts of A . by MSUALG_1:def 2;
J . = id ( the Sorts of A . ) by MSUALG_3:def 1;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in J . by ; :: thesis: verum
end;
hence id the Sorts of A is MSCongruence of A by MSUALG_4:def 4; :: thesis: verum