:: deftheorem Def6 defines 1GateCircStr CIRCCOMB:def 6 :
for f being object
for p being FinSequence
for b₃ being non void strict ManySortedSign holds
( b₃ = 1GateCircStr (p,f) iff ( the carrier of b₃ = (rng p) \/ {[p,f]} & the carrier' of b₃ = {[p,f]} & the Arity of b₃ . [p,f] = p & the ResultSort of b₃ . [p,f] = [p,f] ) );