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

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