for f, x being set
for p being FinSequence holds
( x in the carrier of (1GateCircStr (p,f,x)) & ( for y being set st y in rng p holds
y in the carrier of (1GateCircStr (p,f,x)) ) )