for S being non empty non void ManySortedSign
for s1, s2 being SortSymbol of S
for A being feasible MSAlgebra over S
for f being Function st f is_e.translation_of A,s1,s2 holds
( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} )