for X1, X2 being set
for X being non empty finite set
for n being Element of NAT
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n
for S being Signature of X st rng p = X1 \/ X2 & X1 c= the carrier of S & X2 misses InnerVertices S & not Output (1GateCircStr (p,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (p,f))) = (InputVertices S) \/ X2