let X be non empty finite set ; :: thesis: for n being Nat
for p being FinSeqLen of
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
let n be Nat; :: thesis: for p being FinSeqLen of
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
let p be FinSeqLen of ; :: thesis: 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
let f be Function of (n -tuples_on X),X; :: thesis: for o being OperSymbol of (1GateCircStr p,f)
for s being State of (1GateCircuit p,f) holds o depends_on_in s = s * p
let o be OperSymbol of (1GateCircStr p,f); :: thesis: for s being State of (1GateCircuit p,f) holds o depends_on_in s = s * p
let s be State of (1GateCircuit p,f); :: thesis: o depends_on_in s = s * p
o depends_on_in s = s * (the_arity_of o) by CIRCUIT1:def 3
.= s * p by CIRCCOMB:48 ;
hence o depends_on_in s = s * p ; :: thesis: verum