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

set p = <*x,y,z*>;

set A = the carrier of (1GateCircStr (<*x,y,z*>,f));

y in {x,y,z} by ENUMSET1:def 1;

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

z in {x,y,z} by ENUMSET1:def 1;

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

x in {x,y,z} by ENUMSET1:def 1;

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

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

set p = <*x,y,z*>;

set A = the carrier of (1GateCircStr (<*x,y,z*>,f));

y in {x,y,z} by ENUMSET1:def 1;

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

z in {x,y,z} by ENUMSET1:def 1;

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

x in {x,y,z} by ENUMSET1:def 1;

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

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