:: deftheorem Def5 defines -Terms MSAFREE3:def 5 :
for S being non void Signature
for Y being non-empty ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for b₄ being MSSubset of (FreeMSA Y) holds
( b₄ = S -Terms (X,Y) iff for s being SortSymbol of S holds b₄ . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } );