:: deftheorem Def6 defines Translation MSUALG_6:def 6 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for b₅ being Function of ( the Sorts of A . s1),( the Sorts of A . s2) holds
( b₅ is Translation of A,s1,s2 iff ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st
( b₅ = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) ) );