let C be initialized ConstructorSignature; :: thesis: for a being expression of C, an_Adj C holds
( (non_op C) term a is expression of C, an_Adj C & (non_op C) term a = [non_op, the carrier of C] -tree <*a*> )
let a be expression of C, an_Adj C; :: thesis: ( (non_op C) term a is expression of C, an_Adj C & (non_op C) term a = [non_op, the carrier of C] -tree <*a*> )
A1: the_result_sort_of (non_op C) = an_Adj C by Def9;
A2: the_arity_of (non_op C) = <*(an_Adj C)*> by Def9;
then A3: len (the_arity_of (non_op C)) = 1 by FINSEQ_1:40;
A4: (the_arity_of (non_op C)) . 1 = an_Adj C by A2;
then (non_op C) term a = [non_op, the carrier of C] -tree <*a*> by A3, Def30;
hence ( (non_op C) term a is expression of C, an_Adj C & (non_op C) term a = [non_op, the carrier of C] -tree <*a*> ) by A1, A3, A4, Th42; :: thesis: verum