let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R, E being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in E . s iff a,b are_convertible_wrt (TRS R) . s ) ) holds
E is EquationalTheory of A
let A be non-empty MSAlgebra over S; :: thesis: for R, E being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in E . s iff a,b are_convertible_wrt (TRS R) . s ) ) holds
E is EquationalTheory of A
let R, E be ManySortedRelation of A; :: thesis: ( ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in E . s iff a,b are_convertible_wrt (TRS R) . s ) ) implies E is EquationalTheory of A )
assume A1: for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in E . s iff a,b are_convertible_wrt (TRS R) . s ) ; :: thesis: E is EquationalTheory of A
A2: E is stable

proof

let h be Endomorphism of A; :: according to MSUALG_6:def 9 :: thesis: for s being SortSymbol of S
for a, b being set st [a,b] in E . s holds
[((h . s) . a),((h . s) . b)] in E . s
let s be SortSymbol of S; :: thesis: for a, b being set st [a,b] in E . s holds
[((h . s) . a),((h . s) . b)] in E . s
let a, b be set ; :: thesis: ( [a,b] in E . s implies [((h . s) . a),((h . s) . b)] in E . s )
assume A3: [a,b] in E . s ; :: thesis: [((h . s) . a),((h . s) . b)] in E . s
then reconsider x = a, y = b as Element of A,s by ZFMISC_1:87;
reconsider a9 = (h . s) . x, b9 = (h . s) . y as Element of A,s ;
x,y are_convertible_wrt (TRS R) . s by A1, A3;
then a9,b9 are_convertible_wrt (TRS R) . s by Th45;
hence [((h . s) . a),((h . s) . b)] in E . s by A1; :: thesis: verum

end;

A4: E is invariant

proof

let s1, s2 be SortSymbol of S; :: according to MSUALG_6:def 8 :: thesis: for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in E . s1 holds
[(t . a),(t . b)] in E . s2
let t be Function; :: thesis: ( t is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in E . s1 holds
[(t . a),(t . b)] in E . s2 )
assume A5: t is_e.translation_of A,s1,s2 ; :: thesis: for a, b being set st [a,b] in E . s1 holds
[(t . a),(t . b)] in E . s2
then reconsider f = t as Function of ( the Sorts of A . s1),( the Sorts of A . s2) by Th11;
let a, b be set ; :: thesis: ( [a,b] in E . s1 implies [(t . a),(t . b)] in E . s2 )
assume A6: [a,b] in E . s1 ; :: thesis: [(t . a),(t . b)] in E . s2
then reconsider x = a, y = b as Element of A,s1 by ZFMISC_1:87;
x,y are_convertible_wrt (TRS R) . s1 by A1, A6;
then A7: t . x,t . y are_convertible_wrt (TRS R) . s2 by A5, Th47;
A8: t . y = f . y ;
t . x = f . x ;
hence [(t . a),(t . b)] in E . s2 by A1, A8, A7; :: thesis: verum

end;

E is MSEquivalence_Relation-like by A1, Th49;
hence E is EquationalTheory of A by A2, A4, MSUALG_4:def 3; :: thesis: verum