consider m, a being OperSymbol of C such that
A1: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by ABCMIZ_1:def 12;
( the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> & the_arity_of (non_op C) = <*(an_Adj C)*> ) by ABCMIZ_1:38;
then reconsider m = m as constructor OperSymbol of C by A1, ABCMIZ_1:def 11;
set p = <*> (QuasiTerms C);
take e = m -trm (<*> (QuasiTerms C)); :: thesis: e is constructor
thus e is compound ; :: according to ABCMIZ_A:def 11 :: thesis: main-constr e is constructor OperSymbol of C
len (<*> (QuasiTerms C)) = len (the_arity_of m) by A1;
hence main-constr e is constructor OperSymbol of C by Th35; :: thesis: verum