let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S holds [| the Sorts of A, the Sorts of A|] is MSCongruence of A

let A be non-empty MSAlgebra over 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)

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)

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)

let A be non-empty MSAlgebra over 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

then reconsider J = [| the Sorts of A, the Sorts of A|] as ManySortedRelation of the Sorts of A by MSUALG_4:def 1;
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 16;

hence [| the Sorts of A, the Sorts of A|] . i is Relation of ( the Sorts of A . i) ; :: thesis: verum

end;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 16;

hence [| the Sorts of A, the Sorts of A|] . i is Relation of ( the Sorts of A . i) ; :: thesis: verum

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

then reconsider J = J as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A by MSUALG_4:def 2;
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 16;

hence R is Equivalence_Relation of ( the Sorts of A . i) by A2; :: thesis: verum

end;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 16;

hence R is Equivalence_Relation of ( the Sorts of A . i) by A2; :: thesis: verum

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

hence
[| the Sorts of A, the Sorts of A|] is MSCongruence of A
by MSUALG_4:def 4; :: thesis: verum
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 5;

then (Den (o,A)) . y in the Sorts of A . ( the ResultSort of S . o) by A3, FUNCT_1:13;

then A4: (Den (o,A)) . y in the Sorts of A . (the_result_sort_of o) by MSUALG_1:def 2;

(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 5;

then (Den (o,A)) . x in the Sorts of A . ( the ResultSort of S . o) by A3, FUNCT_1:13;

then A5: (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) = [:( the Sorts of A . (the_result_sort_of o)),( the Sorts of A . (the_result_sort_of o)):] by PBOOLE:def 16;

hence [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) by A5, A4, ZFMISC_1:87; :: thesis: verum

end;[(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 5;

then (Den (o,A)) . y in the Sorts of A . ( the ResultSort of S . o) by A3, FUNCT_1:13;

then A4: (Den (o,A)) . y in the Sorts of A . (the_result_sort_of o) by MSUALG_1:def 2;

(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 5;

then (Den (o,A)) . x in the Sorts of A . ( the ResultSort of S . o) by A3, FUNCT_1:13;

then A5: (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) = [:( the Sorts of A . (the_result_sort_of o)),( the Sorts of A . (the_result_sort_of o)):] by PBOOLE:def 16;

hence [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) by A5, A4, ZFMISC_1:87; :: thesis: verum