for S being non empty non void ManySortedSign
for s1, s2 being SortSymbol of S
for A being non-empty MSAlgebra over S st [s1,s2] in TranslationRel S holds
ex f being Function st f is_e.translation_of A,s1,s2