let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S holds [|the Sorts of A,the Sorts of A|] is MSCongruence of A
let A be non-empty MSAlgebra of S; :: thesis: [|the Sorts of A,the Sorts of A|] is MSCongruence of A
set J = [|the Sorts of A,the Sorts of A|];
for i being set st i in the carrier of S holds
[|the Sorts of A,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 [|the Sorts of A,the Sorts of A|] . i is Relation of (the Sorts of A . i) )
assume i in the carrier of S ; :: thesis: [|the Sorts of A,the Sorts of A|] . i is Relation of (the Sorts of A . i)
then [|the Sorts of A,the Sorts of A|] . i c= [:(the Sorts of A . i),(the Sorts of A . i):] by PBOOLE:def 21;
hence [|the Sorts of A,the Sorts of A|] . i is Relation of (the Sorts of A . i) ; :: thesis: verum

end;

then reconsider J = [|the Sorts of A,the Sorts of A|] as ManySortedRelation of the Sorts of A by MSUALG_4:def 2;
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 = nabla (the Sorts of A . i) by A1, PBOOLE:def 21;
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 3;
reconsider J = J as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 5;
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 . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . y)] in J . (the_result_sort_of o)

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 . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . y)] in J . (the_result_sort_of o)
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 . ((the_arity_of o) /. n) ) implies [((Den o,A) . x),((Den o,A) . y)] in J . (the_result_sort_of o) )
assume for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . ((the_arity_of o) /. n) ; :: thesis: [((Den o,A) . x),((Den o,A) . y)] in J . (the_result_sort_of o)
o in the carrier' of S ;
then A3: o in dom the ResultSort of S by FUNCT_2:def 1;
(Den o,A) . y in Result o,A ;
then (Den o,A) . y in (the Sorts of A * the ResultSort of S) . o by MSUALG_1:def 10;
then (Den o,A) . y in the Sorts of A . (the ResultSort of S . o) by A3, FUNCT_1:23;
then A4: (Den o,A) . y in the Sorts of A . (the_result_sort_of o) by MSUALG_1:def 7;
(Den o,A) . x in Result o,A ;
then (Den o,A) . x in (the Sorts of A * the ResultSort of S) . o by MSUALG_1:def 10;
then (Den o,A) . x in the Sorts of A . (the ResultSort of S . o) by A3, FUNCT_1:23;
then A5: (Den o,A) . x in the Sorts of A . (the_result_sort_of o) by MSUALG_1:def 7;
J . (the_result_sort_of o) = [:(the Sorts of A . (the_result_sort_of o)),(the Sorts of A . (the_result_sort_of o)):] by PBOOLE:def 21;
hence [((Den o,A) . x),((Den o,A) . y)] in J . (the_result_sort_of o) by A5, A4, ZFMISC_1:106; :: thesis: verum

end;

hence [|the Sorts of A,the Sorts of A|] is MSCongruence of A by MSUALG_4:def 6; :: thesis: verum