theorem Th57: :: ABCMIZ_A:57

for n being Nat
for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s st len (the_arity_of m) = n