:: deftheorem Def31 defines term ABCMIZ_1:def 31 :
for C being initialized ConstructorSignature
for o being OperSymbol of C st len (the_arity_of o) = 2 holds
for e1, e2 being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & e1 is expression of C,s1 & e2 is expression of C,s2 ) holds
o term (e1,e2) = [o, the carrier of C] -tree <*e1,e2*>;