theorem :: ABCMIZ_A:44

for m being constructor unary OperSymbol of MaxConstrSign
for t being quasi-term holds main-constr (m term t) = m