for S being non empty non void ManySortedSign
for U1 being MSAlgebra over S
for s being SortSymbol of S
for R being MSEquivalence-like ManySortedRelation of U1 holds R . s is Equivalence_Relation of ( the Sorts of U1 . s) by Def3, Def2;