theorem Th65: :: ABCMIZ_1:65

for C being initialized ConstructorSignature
for a being positive quasi-adjective of C ex v being constructor OperSymbol of C st
( the_result_sort_of v = an_Adj C & ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of v) & a = v -trm p ) )