for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being stable ManySortedRelation of A
for s being SortSymbol of S
for a, b being Element of A,s st a,b are_convertible_wrt R . s holds
for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s