:: deftheorem Def4 defines arity COMPUT_1:def 4 :
for F being with_the_same_arity Relation
for b₂ being Element of NAT holds
( ( ex f being homogeneous Function st f in rng F implies ( b₂ = arity F iff for f being homogeneous Function st f in rng F holds
b₂ = arity f ) ) & ( ( for f being homogeneous Function holds not f in rng F ) implies ( b₂ = arity F iff b₂ = 0 ) ) );