theorem Th11: :: PRALG_1:11

for J being non empty set
for B being non-empty ManySortedSet of J
for O being ManySortedOperation of B holds
( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) )