:: deftheorem Def7 defines unsplit CIRCCOMB:def 7 :
for IT being ManySortedSign holds
( IT is unsplit iff the ResultSort of IT = id the carrier' of IT );