theorem :: MSUALG_6:38

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st
( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) )