theorem :: CIRCCOMB:38

for f, x being set
for p being FinSequence holds
( InputVertices (1GateCircStr (p,f,x)) = (rng p) \ {x} & InnerVertices (1GateCircStr (p,f,x)) = {x} )