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

( 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