:: deftheorem defines -omitting MSAFREE5:def 41 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for B being non empty FinSequence of the carrier of S
for D being b₃ -sorts FinSequence of (Free (S,X))
for V being b₃ -sorts FinSequence of Union X holds
( V is D -omitting iff for t being Element of (Free (S,X)) st t in rng D holds
vf t misses rng V );