:: deftheorem Def25 defines arity MARGREL1:def 25 :
for f being homogeneous Relation
for b₂ being Nat holds
( ( ex x being FinSequence st x in dom f implies ( b₂ = arity f iff for x being FinSequence st x in dom f holds
b₂ = len x ) ) & ( ( for x being FinSequence holds not x in dom f ) implies ( b₂ = arity f iff b₂ = 0 ) ) );