for S being non empty non void ManySortedSign
for U0, U1 being non-empty MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds
U1 |= e