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