:: deftheorem defines -ary_oper_including MSAFREE5:def 6 :
for n being Nat
for S being non empty non void ManySortedSign holds
( S is n -ary_oper_including iff ex o being OperSymbol of S st len (the_arity_of o) = n );