:: deftheorem defines is_of_type AOFA_A00:def 8 :
for S being ManySortedSign
for o, a being set
for r being Element of S holds
( o is_of_type a,r iff ( the Arity of S . o = a & the ResultSort of S . o = r ) );