theorem Th1: :: CIRCCMB2:1

for X being non empty finite set
for n being Nat
for p being FinSeqLen of n
for f being Function of (n -tuples_on X),X
for o being OperSymbol of (1GateCircStr (p,f))
for s being State of (1GateCircuit (p,f)) holds o depends_on_in s = s * p