for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for V being Variables of A
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
for v being Element of V . s holds x <> v