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 by Def9;
A2: the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> by Def9;
then A3: len (the_arity_of (ast C)) = 2 by FINSEQ_1:44;
A4: (the_arity_of (ast C)) . 1 = an_Adj C by A2, FINSEQ_1:44;
A5: (the_arity_of (ast C)) . 2 = a_Type C by A2, FINSEQ_1:44;
then (ast C) term (a,t) = [*, the carrier of C] -tree <*a,t*> by A3, A4, Def31;
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, A3, A4, A5, Th45; :: thesis: verum