:: deftheorem defines FreeSort MSAFREE:def 10 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeSort (X,s) = { a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } ;