let x, y, f be object ; :: thesis: ( x in the carrier of (1GateCircStr (<*x,y*>,f)) & y in the carrier of (1GateCircStr (<*x,y*>,f)) & [<*x,y*>,f] in the carrier of (1GateCircStr (<*x,y*>,f)) )

set p = <*x,y*>;

x in {x,y} by TARSKI:def 2;

then A1: x in rng <*x,y*> by FINSEQ_2:127;

y in {x,y} by TARSKI:def 2;

then A2: y in rng <*x,y*> by FINSEQ_2:127;

( the carrier of (1GateCircStr (<*x,y*>,f)) = (rng <*x,y*>) \/ {[<*x,y*>,f]} & [<*x,y*>,f] in {[<*x,y*>,f]} ) by CIRCCOMB:def 6, TARSKI:def 1;

hence ( x in the carrier of (1GateCircStr (<*x,y*>,f)) & y in the carrier of (1GateCircStr (<*x,y*>,f)) & [<*x,y*>,f] in the carrier of (1GateCircStr (<*x,y*>,f)) ) by A1, A2, XBOOLE_0:def 3; :: thesis: verum

set p = <*x,y*>;

x in {x,y} by TARSKI:def 2;

then A1: x in rng <*x,y*> by FINSEQ_2:127;

y in {x,y} by TARSKI:def 2;

then A2: y in rng <*x,y*> by FINSEQ_2:127;

( the carrier of (1GateCircStr (<*x,y*>,f)) = (rng <*x,y*>) \/ {[<*x,y*>,f]} & [<*x,y*>,f] in {[<*x,y*>,f]} ) by CIRCCOMB:def 6, TARSKI:def 1;

hence ( x in the carrier of (1GateCircStr (<*x,y*>,f)) & y in the carrier of (1GateCircStr (<*x,y*>,f)) & [<*x,y*>,f] in the carrier of (1GateCircStr (<*x,y*>,f)) ) by A1, A2, XBOOLE_0:def 3; :: thesis: verum