set C = MaxConstrSign ;
let m be nullary OperSymbol of MaxConstrSign; :: thesis: main-constr (m term) = m
the_arity_of m = 0 by Def13;
then ( len (the_arity_of m) = 0 & len {} = 0 ) ;
then A1: ( m term = [m, the carrier of MaxConstrSign] -tree {} & m -trm (<*> (QuasiTerms MaxConstrSign)) = [m, the carrier of MaxConstrSign] -tree {} ) by ABCMIZ_1:def 29, ABCMIZ_1:def 35;
hence main-constr (m term) = ((m term) . {}) `1 by Def9
.= [m, the carrier of MaxConstrSign] `1 by A1, TREES_4:def 4
.= m ;
:: thesis: verum