theorem Th41: :: CIRCCOMB:41

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