theorem :: CIRCCOMB:37

for f, x being set
for p being FinSequence
for g being Gate of (1GateCircStr (p,f,x)) holds
( g = [p,f] & the_arity_of g = p & the_result_sort_of g = x )