let S, S' be non empty non void ManySortedSign ; :: thesis: for f being Function of the carrier of S',the carrier of S
for g being Function st f,g form_morphism_between S',S holds
for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2
consider A being non-empty MSAlgebra of S;
let f be Function of the carrier of S',the carrier of S; :: thesis: for g being Function st f,g form_morphism_between S',S holds
for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2
let g be Function; :: thesis: ( f,g form_morphism_between S',S implies for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2 )
assume A1: f,g form_morphism_between S',S ; :: thesis: for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2
then A | S',f,g is non-empty MSAlgebra of S' by Th23;
hence for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2 by A1, Lm1; :: thesis: verum