:: deftheorem Def9 defines main-constr ABCMIZ_A:def 9 :
for S being non empty non void ManySortedSign
for X being V6() ManySortedSet of the carrier of S
for e being Element of (Free (S,X)) holds
( ( e is compound implies main-constr e = (e . {}) `1 ) & ( not e is compound implies main-constr e = {} ) );