let f, x be set ; :: thesis: 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; :: thesis: ( 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; :: thesis: verum