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 Def14;
then the_arity_of m = 1 |-> a_Term by ABCMIZ_1:37
.= <*a_Term*> by FINSEQ_2:59 ;
then ( len p = 1 & (the_arity_of m) . 1 = a_Term MaxConstrSign ) by FINSEQ_1:40;
then A2: ( 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;
hence main-constr (m term t) = ((m term t) . {}) `1 by Def9
.= [m, the carrier of MaxConstrSign] `1 by A2, TREES_4:def 4
.= m ;
:: thesis: verum