:: deftheorem Def9 defines gate`2isBoolean CIRCCOMB:def 9 :
for IT being ManySortedSign holds
( IT is gate`2isBoolean iff for g being set st g in the carrier' of IT holds
for p being FinSequence st p = the Arity of IT . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] );