for C being initialized ConstructorSignature
for q being pure expression of C, a_Type C ex m being constructor OperSymbol of C st
( the_result_sort_of m = a_Type C & ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of m) & q = m -trm p ) )