for S being one-gate ManySortedSign
for A being one-gate Circuit of S
for n being Element of NAT
for X being non empty finite set
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n st A = 1GateCircuit (p,f) holds
S = 1GateCircStr (p,f)