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