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