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