for S being non empty non void ManySortedSign
for s being SortSymbol of S
for o being OperSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) holds
( ( for i being Nat st i in dom p holds
p /. i is x -omitting ) iff o -term p is x -omitting )