let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for h being Endomorphism of A
for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for a being Element of Args o,A holds (h . (the_result_sort_of o)) * (transl o,i,a,A) = (transl o,i,(h # a),A) * (h . ((the_arity_of o) /. i))
let A be non-empty MSAlgebra of S; :: thesis: for h being Endomorphism of A
for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for a being Element of Args o,A holds (h . (the_result_sort_of o)) * (transl o,i,a,A) = (transl o,i,(h # a),A) * (h . ((the_arity_of o) /. i))
let h be Endomorphism of A; :: thesis: for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for a being Element of Args o,A holds (h . (the_result_sort_of o)) * (transl o,i,a,A) = (transl o,i,(h # a),A) * (h . ((the_arity_of o) /. i))
h is_homomorphism A,A by Def2;
hence for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for a being Element of Args o,A holds (h . (the_result_sort_of o)) * (transl o,i,a,A) = (transl o,i,(h # a),A) * (h . ((the_arity_of o) /. i)) by Th21; :: thesis: verum