:: deftheorem Def9 defines constructor ABCMIZ_1:def 9 :
for C being Signature holds
( C is constructor iff ( the carrier of C = {a_Type,an_Adj,a_Term} & {*,non_op} c= the carrier' of C & the Arity of C . * = <*an_Adj,a_Type*> & the Arity of C . non_op = <*an_Adj*> & the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( for o being Element of the carrier' of C st o <> * & o <> non_op holds
the Arity of C . o in {a_Term} * ) ) );