theorem :: ABCMIZ_1:37

for S being ConstructorSignature
for o being OperSymbol of S st o is constructor holds
the_arity_of o = (len (the_arity_of o)) |-> a_Term