let S, S9 be non empty non void ManySortedSign ; :: thesis: 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 s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds

TranslationRel S reduces f . s1,f . s2

set A = the non-empty MSAlgebra over S;

let f be Function of the carrier of S9, the carrier of S; :: thesis: for g being Function st f,g form_morphism_between S9,S holds

for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds

TranslationRel S reduces f . s1,f . s2

let g be Function; :: thesis: ( f,g form_morphism_between S9,S implies for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds

TranslationRel S reduces f . s1,f . s2 )

assume A1: f,g form_morphism_between S9,S ; :: thesis: for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds

TranslationRel S reduces f . s1,f . s2

then the non-empty MSAlgebra over S | (S9,f,g) is non-empty MSAlgebra over S9 by Th22;

hence for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds

TranslationRel S reduces f . s1,f . s2 by A1, Lm1; :: thesis: verum

for g being Function st f,g form_morphism_between S9,S holds

for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds

TranslationRel S reduces f . s1,f . s2

set A = the non-empty MSAlgebra over S;

let f be Function of the carrier of S9, the carrier of S; :: thesis: for g being Function st f,g form_morphism_between S9,S holds

for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds

TranslationRel S reduces f . s1,f . s2

let g be Function; :: thesis: ( f,g form_morphism_between S9,S implies for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds

TranslationRel S reduces f . s1,f . s2 )

assume A1: f,g form_morphism_between S9,S ; :: thesis: for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds

TranslationRel S reduces f . s1,f . s2

then the non-empty MSAlgebra over S | (S9,f,g) is non-empty MSAlgebra over S9 by Th22;

hence for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds

TranslationRel S reduces f . s1,f . s2 by A1, Lm1; :: thesis: verum