set C = MaxConstrSign ;
let m be constructor unary OperSymbol of MaxConstrSign ; :: thesis: for t being quasi-term holds main-constr (m term t) = m
let t be quasi-term; :: thesis: main-constr (m term t) = m
reconsider w = t as Element of QuasiTerms MaxConstrSign by ABCMIZ_1:49;
reconsider p = <*w*> as FinSequence of QuasiTerms MaxConstrSign ;
A1: len (the_arity_of m) = 1 by Udef;
then the_arity_of m = 1 |-> a_Term by ABCMIZ_1:37
.= <*a_Term *> by FINSEQ_2:73 ;
then ( len p = 1 & (the_arity_of m) . 1 = a_Term MaxConstrSign ) by FINSEQ_1:57;
then A0: ( m term t = [m,the carrier of MaxConstrSign ] -tree <*t*> & m -trm p = [m,the carrier of MaxConstrSign ] -tree <*t*> ) by A1, ABCMIZ_1:def 30, ABCMIZ_1:def 35;
thus main-constr (m term t) = ((m term t) . {} ) `1 by A0, MCON
.= [m,the carrier of MaxConstrSign ] `1 by A0, TREES_4:def 4
.= m by MCART_1:7 ; :: thesis: verum