:: deftheorem defines 1GateCircuit CIRCCOMB:def 12 :
for n being Nat
for X, Y being non empty set
for f being Function of (n -tuples_on X),Y
for p being FinSeqLen of n
for x being set st ( x in rng p implies X = Y ) holds
for b₇ being strict non-empty MSAlgebra over 1GateCircStr (p,f,x) holds
( b₇ = 1GateCircuit (p,f,x) iff ( the Sorts of b₇ = ((rng p) --> X) +* (x .--> Y) & the Charact of b₇ . [p,f] = f ) );