let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for h being Endomorphism of A
for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A,s1,s2 holds
ex T being Function of (the Sorts of A . s1),(the Sorts of A . s2) st
( T is_e.translation_of A,s1,s2 & T * (h . s1) = (h . s2) * t )
let A be non-empty MSAlgebra of S; :: thesis: for h being Endomorphism of A
for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A,s1,s2 holds
ex T being Function of (the Sorts of A . s1),(the Sorts of A . s2) st
( T is_e.translation_of A,s1,s2 & T * (h . s1) = (h . s2) * t )
let h be Endomorphism of A; :: thesis: for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A,s1,s2 holds
ex T being Function of (the Sorts of A . s1),(the Sorts of A . s2) st
( T is_e.translation_of A,s1,s2 & T * (h . s1) = (h . s2) * t )
h is_homomorphism A,A by Def2;
hence for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A,s1,s2 holds
ex T being Function of (the Sorts of A . s1),(the Sorts of A . s2) st
( T is_e.translation_of A,s1,s2 & T * (h . s1) = (h . s2) * t ) by Th23; :: thesis: verum