for S being non empty non void ManySortedSign
for X being V5() 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 st V is D -omitting holds
for b1, b2 being Element of dom B holds D . b1 is V . b2 -omitting