let x1, x2, x3 be set ; :: thesis: for X being non empty finite set
for f being Function of (3 -tuples_on X),X
for S being Signature of X st x1 in the carrier of S & x2 in the carrier of S & x3 in the carrier of S & not Output (1GateCircStr <*x1,x2,x3*>,f) in InputVertices S holds
InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = InputVertices S
let X be non empty finite set ; :: thesis: for f being Function of (3 -tuples_on X),X
for S being Signature of X st x1 in the carrier of S & x2 in the carrier of S & x3 in the carrier of S & not Output (1GateCircStr <*x1,x2,x3*>,f) in InputVertices S holds
InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = InputVertices S
let f be Function of (3 -tuples_on X),X; :: thesis: for S being Signature of X st x1 in the carrier of S & x2 in the carrier of S & x3 in the carrier of S & not Output (1GateCircStr <*x1,x2,x3*>,f) in InputVertices S holds
InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = InputVertices S
let S be Signature of X; :: thesis: ( x1 in the carrier of S & x2 in the carrier of S & x3 in the carrier of S & not Output (1GateCircStr <*x1,x2,x3*>,f) in InputVertices S implies InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = InputVertices S )
assume ( x1 in the carrier of S & x2 in the carrier of S & x3 in the carrier of S ) ; :: thesis: ( Output (1GateCircStr <*x1,x2,x3*>,f) in InputVertices S or InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = InputVertices S )
then A1: ( {x1,x2} c= the carrier of S & {x3} c= the carrier of S ) by ZFMISC_1:37, ZFMISC_1:38;
rng <*x1,x2,x3*> = {x1,x2,x3} by FINSEQ_2:148
.= {x1,x2} \/ {x3} by ENUMSET1:43 ;
hence ( Output (1GateCircStr <*x1,x2,x3*>,f) in InputVertices S or InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = InputVertices S ) by A1, Th39, XBOOLE_1:8; :: thesis: verum