:: deftheorem defines -term MSAFREE5:def 14 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for s being SortSymbol of S
for x being Element of X . s holds x -term = root-tree [x,s];