let C be initialized ConstructorSignature; :: thesis: for e being expression of C st e . {} = [non_op, the carrier of C] holds
ex a being expression of C, an_Adj C st e = (non_op C) term a
let e be expression of C; :: thesis: ( e . {} = [non_op, the carrier of C] implies ex a being expression of C, an_Adj C st e = (non_op C) term a )
assume A1: e . {} = [non_op, the carrier of C] ; :: thesis: ex a being expression of C, an_Adj C st e = (non_op C) term a
non_op 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 st e = (non_op C) term a

hence ex a being expression of C, an_Adj C st e = (non_op C) term a 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 st e = (non_op C) term a

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 non_op = c by A1, XTUPLE_0:1;
hence ex a being expression of C, an_Adj C st e = (non_op C) term a 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 st e = (non_op C) term a

hence ex a being expression of C, an_Adj C st e = (non_op C) term a ; :: 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 st e = (non_op C) term a

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

end;

end;