set C = MaxConstrSign ;
set m = ast MaxConstrSign;
let q be expression of MaxConstrSign , a_Type MaxConstrSign; for a being quasi-adjective holds main-constr ((ast MaxConstrSign) term (a,q)) = *
let a be quasi-adjective; main-constr ((ast MaxConstrSign) term (a,q)) = *
A1:
len (the_arity_of (ast MaxConstrSign)) = 2
by Def15;
the_arity_of (ast MaxConstrSign) = <*(an_Adj MaxConstrSign),(a_Type MaxConstrSign)*>
by ABCMIZ_1:38;
then
( (the_arity_of (ast MaxConstrSign)) . 1 = an_Adj MaxConstrSign & (the_arity_of (ast MaxConstrSign)) . 2 = a_Type MaxConstrSign )
by FINSEQ_1:44;
then A2:
(ast MaxConstrSign) term (a,q) = [(ast MaxConstrSign), the carrier of MaxConstrSign] -tree <*a,q*>
by A1, ABCMIZ_1:def 31;
thus main-constr ((ast MaxConstrSign) term (a,q)) =
(((ast MaxConstrSign) term (a,q)) . {}) `1
by Def9
.=
[(ast MaxConstrSign), the carrier of MaxConstrSign] `1
by A2, TREES_4:def 4
.=
*
; verum