let S, S9 be non empty non void ManySortedSign ; 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; 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; ( 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
; 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; verum