for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s1, s2 being SortSymbol of S
for f being Function st f is_e.translation_of A,s1,s2 holds
( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 )