:: deftheorem Def13 defines 1GateCircuit CIRCCOMB:def 13 :
for n being Nat
for X being non empty set
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n
for b₅ being strict non-empty MSAlgebra over 1GateCircStr (p,f) holds
( b₅ = 1GateCircuit (p,f) iff ( the Sorts of b₅ = the carrier of (1GateCircStr (p,f)) --> X & the Charact of b₅ . [p,f] = f ) );