for S, S9 being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 by Lm1;