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 A0: 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 A1: e . {} in [:the carrier' of C,{the carrier of C}:] by A0, ZFMISC_1:129;

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 Th100;

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 A1, COMP; :: 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
A2: ( len p = len (the_arity_of c) & e = c -trm p ) ;
e = [c,the carrier of C] -tree p by A2, TERM;
then e . {} = [c,the carrier of C] by TREES_4:def 4;
then * = c by A0, ZFMISC_1:33;
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 CNSTR2; :: 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
A3: e = (non_op C) term a ;
e = [non_op ,the carrier of C] -tree <*a*> by A3, ThNon;
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 A0, ZFMISC_1:33; :: 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;