set C = MaxConstrSign ;
set m = non_op MaxConstrSign;
let a be quasi-adjective; :: thesis: main-constr ((non_op MaxConstrSign) term a) = non_op
A1: len (the_arity_of (non_op MaxConstrSign)) = 1 by Def14;
the_arity_of (non_op MaxConstrSign) = <*an_Adj*> by ABCMIZ_1:38;
then (the_arity_of (non_op MaxConstrSign)) . 1 = an_Adj MaxConstrSign by FINSEQ_1:40;
then A2: (non_op MaxConstrSign) term a = [(non_op MaxConstrSign), the carrier of MaxConstrSign] -tree <*a*> by A1, ABCMIZ_1:def 30;
thus main-constr ((non_op MaxConstrSign) term a) = (((non_op MaxConstrSign) term a) . {}) `1 by Def9
.= [(non_op MaxConstrSign), the carrier of MaxConstrSign] `1 by A2, TREES_4:def 4
.= non_op ; :: thesis: verum