let S be non empty non void ManySortedSign ; 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; 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)
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)
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 . ((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;
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);
( ( 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 A3:
for
n being
Nat st
n in dom x holds
[(x . n),(y . n)] in J . ((the_arity_of o) /. n)
;
[((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o)
A4:
dom y =
dom (the_arity_of o)
by MSUALG_3:6
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
A5:
dom x =
dom (the_arity_of o)
by MSUALG_3:6
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
then reconsider x9 =
x,
y9 =
y as
FinSequence by A4, FINSEQ_1:def 2;
then A7:
x = y
by A5, A4, FINSEQ_1:13;
(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 A8, FUNCT_1:13;
then A9:
(Den (o,A)) . x in the
Sorts of
A . (the_result_sort_of o)
by MSUALG_1:def 2;
J . (the_result_sort_of o) = id ( the Sorts of A . (the_result_sort_of o))
by MSUALG_3:def 1;
hence
[((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o)
by A7, A9, RELAT_1:def 10;
verum
end;
hence
id the Sorts of A is MSCongruence of A
by MSUALG_4:def 4; verum