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