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 by A2, Th55;
hence v -trm p is pure expression of C, a_Type C ; :: thesis: verum