let C be initialized ConstructorSignature; :: thesis: for p being FinSequence of QuasiTerms C
for m being constructor OperSymbol of C st the_result_sort_of m = a_Type C & len p = len (the_arity_of m) holds
m -trm p is pure expression of C, a_Type C
let p be FinSequence of QuasiTerms C; :: thesis: for m being constructor OperSymbol of C st the_result_sort_of m = a_Type C & len p = len (the_arity_of m) holds
m -trm p is pure expression of C, a_Type C
let v be constructor OperSymbol of C; :: thesis: ( the_result_sort_of v = a_Type C & len p = len (the_arity_of v) implies v -trm p is pure expression of C, a_Type C )
assume A1: the_result_sort_of v = a_Type C ; :: thesis: ( not len p = len (the_arity_of v) or v -trm p is pure expression of C, a_Type C )
assume A2: len p = len (the_arity_of v) ; :: thesis: v -trm p is pure expression of C, a_Type C
then reconsider a = v -trm p as expression of C, a_Type C by A1, Th52;
a is pure

proof

assume ex a9 being expression of C, an_Adj C ex t being expression of C, a_Type C st a = (ast C) term (a9,t) ; :: according to ABCMIZ_1:def 41 :: thesis: contradiction
hence contradiction by A2, Th55; :: thesis: verum

end;

hence v -trm p is pure expression of C, a_Type C ; :: thesis: verum