theorem :: ABCMIZ_A:43

for m being nullary OperSymbol of MaxConstrSign holds main-constr (m term) = m