let x1 be set ; for X being non empty finite set
for f being Function of (1 -tuples_on X),X
for S being Signature of X st x1 in the carrier of S & not Output (1GateCircStr (<*x1*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1*>,f))) = InputVertices S
let X be non empty finite set ; for f being Function of (1 -tuples_on X),X
for S being Signature of X st x1 in the carrier of S & not Output (1GateCircStr (<*x1*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1*>,f))) = InputVertices S
set p = <*x1*>;
let f be Function of (1 -tuples_on X),X; for S being Signature of X st x1 in the carrier of S & not Output (1GateCircStr (<*x1*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1*>,f))) = InputVertices S
let S be Signature of X; ( x1 in the carrier of S & not Output (1GateCircStr (<*x1*>,f)) in InputVertices S implies InputVertices (S +* (1GateCircStr (<*x1*>,f))) = InputVertices S )
assume
x1 in the carrier of S
; ( Output (1GateCircStr (<*x1*>,f)) in InputVertices S or InputVertices (S +* (1GateCircStr (<*x1*>,f))) = InputVertices S )
then
{x1} c= the carrier of S
by ZFMISC_1:31;
then
rng <*x1*> c= the carrier of S
by FINSEQ_1:38;
hence
( Output (1GateCircStr (<*x1*>,f)) in InputVertices S or InputVertices (S +* (1GateCircStr (<*x1*>,f))) = InputVertices S )
by Th35; verum