let C be initialized ConstructorSignature; :: thesis: for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds
( (ast C) term a,t is expression of C, a_Type C & (ast C) term a,t = [* ,the carrier of C] -tree <*a,t*> )
let a be expression of C, an_Adj C; :: thesis: for t being expression of C, a_Type C holds
( (ast C) term a,t is expression of C, a_Type C & (ast C) term a,t = [* ,the carrier of C] -tree <*a,t*> )
let t be expression of C, a_Type C; :: thesis: ( (ast C) term a,t is expression of C, a_Type C & (ast C) term a,t = [* ,the carrier of C] -tree <*a,t*> )
A1: ( the_result_sort_of (ast C) = a_Type C & the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> ) by CONSTRSIGN;
then A2: ( len (the_arity_of (ast C)) = 2 & (the_arity_of (ast C)) . 1 = an_Adj C & (the_arity_of (ast C)) . 2 = a_Type C ) by FINSEQ_1:61;
then (ast C) term a,t = [* ,the carrier of C] -tree <*a,t*> by TERM2;
hence ( (ast C) term a,t is expression of C, a_Type C & (ast C) term a,t = [* ,the carrier of C] -tree <*a,t*> ) by A1, A2, Th43b; :: thesis: verum