let C be initialized ConstructorSignature; :: thesis:
let q be pure expression of C, a_Type C; :: thesis:
set e = q;

per cases by Th53;

suppose ex x being variable st q = x -term C ; :: thesis:

hence ex m being constructor OperSymbol of C st
( the_result_sort_of m = a_Type C & ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of m) & q = m -trm p ) ) by Th48; :: thesis:

end;

suppose ex c being constructor OperSymbol of C ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of c) & q = c -trm p ) ; :: thesis:

then consider c being constructor OperSymbol of C, p being FinSequence of QuasiTerms C such that
A1: len p = len (the_arity_of c) and
A2: q = c -trm p ;
take c ; :: thesis:
q is expression of C, the_result_sort_of c by A1, A2, Th52;
hence the_result_sort_of c = a_Type C by Th48; :: thesis:
take p ; :: thesis:
thus ( len p = len (the_arity_of c) & q = c -trm p ) by A1, A2; :: thesis:

end;

suppose ex a being expression of C, an_Adj C st q = (non_op C) term a ; :: thesis:

then q is expression of C, an_Adj C by Th43;
hence ex m being constructor OperSymbol of C st
( the_result_sort_of m = a_Type C & ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of m) & q = m -trm p ) ) by Th48; :: thesis:

end;

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

hence ex m being constructor OperSymbol of C st
( the_result_sort_of m = a_Type C & ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of m) & q = m -trm p ) ) by Def41; :: thesis:

end;

end;