theorem :: CIRCCMB3:18

for n being Element of NAT
for X being non empty finite set
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n
for s being State of (1GateCircuit (p,f)) holds (Following s) . (Output (1GateCircStr (p,f))) = f . (s * p)