:: deftheorem Def19 defines ComAr PRALG_1:def 21 :
for J being non empty set
for B being non-empty ManySortedSet of J
for O being equal-arity ManySortedOperation of B
for b₄ being Nat holds
( b₄ = ComAr O iff for j being Element of J holds b₄ = arity (O . j) );