set C = MaxConstrSign ;
let m be constructor binary OperSymbol of MaxConstrSign; for t1, t2 being quasi-term holds main-constr (m term (t1,t2)) = m
let t1, t2 be quasi-term; 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
;
verum