for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for h being Endomorphism of A
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A,s1,s2 ex T being Translation of A,s1,s2 st T * (h . s1) = (h . s2) * t by Def2, Th25;