set C = MaxConstrSign ;
let m be nullary OperSymbol of MaxConstrSign ; :: thesis: main-constr (m term ) = m
the_arity_of m = 0 by Ndef;
then ( len (the_arity_of m) = 0 & len {} = 0 ) ;
then A0: ( 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 MCON
.= [m,the carrier of MaxConstrSign ] `1 by A0, TREES_4:def 4
.= m by MCART_1:7 ;
:: thesis: verum