let x1, x2, x3 be set ; 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 ; 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; 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; ( 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 )
; ( 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:31, ZFMISC_1:32;
rng <*x1,x2,x3*> =
{x1,x2,x3}
by FINSEQ_2:128
.=
{x1,x2} \/ {x3}
by ENUMSET1:3
;
hence
( Output (1GateCircStr (<*x1,x2,x3*>,f)) in InputVertices S or InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = InputVertices S )
by A1, Th35, XBOOLE_1:8; verum