:: deftheorem Def35 defines -trm ABCMIZ_1:def 35 :
for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p = [c, the carrier of C] -tree p;