:: deftheorem defines finitely_operated MSSCYC_1:def 5 :
for IT being non empty non void ManySortedSign holds
( IT is finitely_operated iff for s being SortSymbol of IT holds { o where o is OperSymbol of IT : the_result_sort_of o = s } is finite );