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 & the_arity_of (non_op C) = <*(an_Adj C)*> ) by CONSTRSIGN;
then A2: ( len (the_arity_of (non_op C)) = 1 & (the_arity_of (non_op C)) . 1 = an_Adj C ) by FINSEQ_1:57;
then (non_op C) term a = [non_op ,the carrier of C] -tree <*a*> by TERM1;
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, A2, Th43a; :: thesis: verum