:: deftheorem SORTS defines -sorts MSAFREE5:def 36 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for B being FinSequence of the carrier of S
for V being FinSequence of Union X holds
( V is B -sorts iff ( dom V = dom B & ( for i being Nat st i in dom B holds
V . i in X . (B . i) ) ) );