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 Bdef;
then the_arity_of m = 2 |-> a_Term by ABCMIZ_1:37
.= <*a_Term ,a_Term *> by FINSEQ_2:75 ;
then ( (the_arity_of m) . 1 = a_Term MaxConstrSign & (the_arity_of m) . 2 = a_Term MaxConstrSign & len p = 2 ) by FINSEQ_1:61;
then A0: ( 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 MCON
.= [m,the carrier of MaxConstrSign ] `1 by A0, TREES_4:def 4
.= m by MCART_1:7 ;
:: thesis: verum