consider v being constructor OperSymbol of C such that
A0: the_result_sort_of v = an_Adj C and
A1: ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of v) & a = v -trm p ) by ThPos;
consider p being FinSequence of QuasiTerms C such that
A2: ( len p = len (the_arity_of v) & a = v -trm p ) by A1;
( len (p at f) = len p & a at f = v -trm (p at f) ) by A2, ThS1, ThTr2;
hence for b₁ being expression of C, an_Adj C st b₁ = a at f holds
b₁ is positive by A0, A2, ThPos2; :: thesis: verum