:: deftheorem defines finite-yielding MSAFREE2:def 11 :
for S being non empty ManySortedSign
for IT being MSAlgebra over S holds
( IT is finite-yielding iff the Sorts of IT is finite-yielding );