let f, x be 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)) ) )
let p be FinSequence; ( 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)) ) )
set A = the carrier of (1GateCircStr (p,f,x));
( the carrier of (1GateCircStr (p,f,x)) = (rng p) \/ {x} & x in {x} )
by CIRCCOMB:def 5, TARSKI:def 1;
hence
( 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)) ) )
by XBOOLE_0:def 3; verum