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 A0: 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 A1: 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 A0, Th43c;
a is positive

proof

assume ex a' being expression of C, an_Adj C st a = (non_op C) term a' ; :: according to ABCMIZ_1:def 37 :: thesis: contradiction
hence contradiction by A1, ThDiff01; :: thesis: verum

end;

then a is positive expression of C, an_Adj C ;
hence v -trm p is positive quasi-adjective of C ; :: thesis: verum