let C be initialized ConstructorSignature; :: thesis: for e being expression of C st e . {} = [*, the carrier of C] holds
ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t)
let e be expression of C; :: thesis: ( e . {} = [*, the carrier of C] implies ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t) )
assume A1: e . {} = [*, the carrier of C] ; :: thesis: ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t)
ast C in the carrier' of C ;
then A2: e . {} in [: the carrier' of C,{ the carrier of C}:] by A1, ZFMISC_1:106;

per cases ( ex x being variable st e = x -term C or ex c being constructor OperSymbol of C ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of c) & e = c -trm p ) or ex a being expression of C, an_Adj C st e = (non_op C) term a or ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t) ) by Th53;

suppose ex x being variable st e = x -term C ; :: thesis: ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t)

hence ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t) by A2, Def27; :: thesis: verum

end;

suppose ex c being constructor OperSymbol of C ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of c) & e = c -trm p ) ; :: thesis: ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t)

then consider c being constructor OperSymbol of C, p being FinSequence of QuasiTerms C such that
A3: len p = len (the_arity_of c) and
A4: e = c -trm p ;
e = [c, the carrier of C] -tree p by A3, A4, Def35;
then e . {} = [c, the carrier of C] by TREES_4:def 4;
then * = c by A1, XTUPLE_0:1;
hence ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t) by Def11; :: thesis: verum

end;

suppose ex a being expression of C, an_Adj C st e = (non_op C) term a ; :: thesis: ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t)

then consider a being expression of C, an_Adj C such that
A5: e = (non_op C) term a ;
e = [non_op, the carrier of C] -tree <*a*> by A5, Th43;
then e . {} = [non_op, the carrier of C] by TREES_4:def 4;
hence ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t) by A1, XTUPLE_0:1; :: thesis: verum

end;

suppose ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t) ; :: thesis: ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t)

hence ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t) ; :: thesis: verum

end;

end;