theorem :: FACIRC_1:46

for f, x being set
for p being FinSequence holds
( 1GateCircStr (p,f,x) is gate`1=arity & 1GateCircStr (p,f,x) is Circuit-like )