for S being non empty non void ManySortedSign
for s being SortSymbol of S
for Y being infinite-yielding ManySortedSet of the carrier of S
for A being finite Subset of (Union the Sorts of (Free (S,Y))) ex y being Element of Y . s st
for v being Element of (Free (S,Y)) st v in A holds
v is y -omitting