let C be initialized ConstructorSignature; :: thesis:
let e be positive quasi-adjective of C; :: thesis:

per cases by Th53;

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

hence ex v being constructor OperSymbol of C st
( the_result_sort_of v = an_Adj C & ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of v) & e = v -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) & e = 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: e = c -trm p ;
take c ; :: thesis:
e is expression of C, the_result_sort_of c by A1, A2, Th52;
hence the_result_sort_of c = an_Adj C by Th48; :: thesis:
take p ; :: thesis:
thus ( len p = len (the_arity_of c) & e = c -trm p ) by A1, A2; :: thesis:

end;

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

hence ex v being constructor OperSymbol of C st
( the_result_sort_of v = an_Adj C & ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of v) & e = v -trm p ) ) by Def37; :: thesis:

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:

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

end;

end;