:: deftheorem Def6 defines -terms MSAFREE4:def 6 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being MSAlgebra over S holds
( A is X,S -terms iff the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X)) );