:: deftheorem DEP defines -dependent MSAFREE5:def 25 :
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for o being OperSymbol of S holds
( o is s -dependent iff s in rng (the_arity_of o) );