for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s holds e `2 in the Sorts of (TermAlg S) . s