let n be Element of NAT ; :: thesis: for X being non empty finite set
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n
for S being Signature of X st rng p c= the carrier of S & not Output (1GateCircStr (p,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (p,f))) = InputVertices S
let X be non empty finite set ; :: thesis: for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n
for S being Signature of X st rng p c= the carrier of S & not Output (1GateCircStr (p,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (p,f))) = InputVertices S
let f be Function of (n -tuples_on X),X; :: thesis: for p being FinSeqLen of n
for S being Signature of X st rng p c= the carrier of S & not Output (1GateCircStr (p,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (p,f))) = InputVertices S
let p be FinSeqLen of n; :: thesis: for S being Signature of X st rng p c= the carrier of S & not Output (1GateCircStr (p,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (p,f))) = InputVertices S
let S be Signature of X; :: thesis: ( rng p c= the carrier of S & not Output (1GateCircStr (p,f)) in InputVertices S implies InputVertices (S +* (1GateCircStr (p,f))) = InputVertices S )
assume that
A1: rng p c= the carrier of S and
A2: not Output (1GateCircStr (p,f)) in InputVertices S ; :: thesis: InputVertices (S +* (1GateCircStr (p,f))) = InputVertices S
A3: the carrier of S = (InputVertices S) \/ (InnerVertices S) by XBOOLE_1:45;
thus InputVertices (S +* (1GateCircStr (p,f))) = ((InputVertices S) \ (InnerVertices (1GateCircStr (p,f)))) \/ ((InputVertices (1GateCircStr (p,f))) \ (InnerVertices S)) by CIRCCMB2:5, CIRCCOMB:47
.= ((InputVertices S) \ (InnerVertices (1GateCircStr (p,f)))) \/ ((rng p) \ (InnerVertices S)) by CIRCCOMB:42
.= ((InputVertices S) \ {(Output (1GateCircStr (p,f)))}) \/ ((rng p) \ (InnerVertices S)) by Th16
.= (InputVertices S) \/ ((rng p) \ (InnerVertices S)) by A2, ZFMISC_1:57
.= InputVertices S by A1, A3, XBOOLE_1:12, XBOOLE_1:43 ; :: thesis: verum