theorem Th12: :: CIRCCMB3:12

for x being set
for X being non empty finite set
for n being Element of NAT
for p being FinSeqLen of n
for g being Function of (n -tuples_on X),X
for s being State of (1GateCircuit (p,g)) holds s * p is Element of n -tuples_on X