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 holds
( the Charact of (1GateCircuit (p,f)) = (p,f) .--> f & ( for v being Vertex of (1GateCircStr (p,f)) holds the Sorts of (1GateCircuit (p,f)) . v = X ) )