:: deftheorem Def11 defines FreeSort MSAFREE:def 11 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for b₃ being ManySortedSet of the carrier of S holds
( b₃ = FreeSort X iff for s being SortSymbol of S holds b₃ . s = FreeSort (X,s) );