set C = MaxConstrSign ;
let m be constructor binary OperSymbol of MaxConstrSign; :: thesis: for t1, t2 being quasi-term holds main-constr (m term (t1,t2)) = m
let t1, t2 be quasi-term; :: thesis: main-constr (m term (t1,t2)) = m
reconsider w1 = t1, w2 = t2 as Element of QuasiTerms MaxConstrSign by ABCMIZ_1:49;
reconsider p = <*w1,w2*> as FinSequence of QuasiTerms MaxConstrSign ;
A1: len (the_arity_of m) = 2 by Def15;
then the_arity_of m = 2 |-> a_Term by ABCMIZ_1:37
.= <*a_Term,a_Term*> by FINSEQ_2:61 ;
then ( (the_arity_of m) . 1 = a_Term MaxConstrSign & (the_arity_of m) . 2 = a_Term MaxConstrSign & len p = 2 ) by FINSEQ_1:44;
then A2: ( m term (t1,t2) = [m, the carrier of MaxConstrSign] -tree <*t1,t2*> & m -trm p = [m, the carrier of MaxConstrSign] -tree p ) by A1, ABCMIZ_1:def 31, ABCMIZ_1:def 35;
hence main-constr (m term (t1,t2)) = ((m term (t1,t2)) . {}) `1 by Def9
.= [m, the carrier of MaxConstrSign] `1 by A2, TREES_4:def 4
.= m ;
:: thesis: verum