:: deftheorem Def12 defines arity-rich ABCMIZ_A:def 12 :
for C being non void Signature holds
( C is arity-rich iff for n being Nat
for s being SortSymbol of C holds { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite );