let X be non empty finite set ; :: thesis: 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
let n be Nat; :: thesis: 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
let p be FinSeqLen of n; :: 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:41 ;
hence o depends_on_in s = s * p ; :: thesis: verum