:: deftheorem SORTS2 defines -sorts MSAFREE5:def 37 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for B being FinSequence of the carrier of S
for D being FinSequence of (Free (S,X)) holds
( D is B -sorts iff ( dom D = dom B & ( for i being Nat st i in dom B holds
D . i in the Sorts of (Free (S,X)) . (B . i) ) ) );