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