let x, y, z be object ; for X being non empty finite set
for f being Function of (3 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y,z*>,f)) holds
( (Following s) . [<*x,y,z*>,f] = f . <*(s . x),(s . y),(s . z)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z )
let X be non empty finite set ; for f being Function of (3 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y,z*>,f)) holds
( (Following s) . [<*x,y,z*>,f] = f . <*(s . x),(s . y),(s . z)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z )
let f be Function of (3 -tuples_on X),X; for s being State of (1GateCircuit (<*x,y,z*>,f)) holds
( (Following s) . [<*x,y,z*>,f] = f . <*(s . x),(s . y),(s . z)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z )
let s be State of (1GateCircuit (<*x,y,z*>,f)); ( (Following s) . [<*x,y,z*>,f] = f . <*(s . x),(s . y),(s . z)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z )
set p = <*x,y,z*>;
dom s = the carrier of (1GateCircStr (<*x,y,z*>,f))
by CIRCUIT1:3;
then A1:
dom s = (rng <*x,y,z*>) \/ {[<*x,y,z*>,f]}
by CIRCCOMB:def 6;
y in {x,y,z}
by ENUMSET1:def 1;
then
y in rng <*x,y,z*>
by FINSEQ_2:128;
then A2:
y in dom s
by A1, XBOOLE_0:def 3;
x in {x,y,z}
by ENUMSET1:def 1;
then
x in rng <*x,y,z*>
by FINSEQ_2:128;
then A3:
x in dom s
by A1, XBOOLE_0:def 3;
z in {x,y,z}
by ENUMSET1:def 1;
then
z in rng <*x,y,z*>
by FINSEQ_2:128;
then A4:
z in dom s
by A1, XBOOLE_0:def 3;
thus (Following s) . [<*x,y,z*>,f] =
f . (s * <*x,y,z*>)
by CIRCCOMB:56
.=
f . <*(s . x),(s . y),(s . z)*>
by A3, A2, A4, FINSEQ_2:126
; ( (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z )
reconsider x = x, y = y, z = z as Vertex of (1GateCircStr (<*x,y,z*>,f)) by Th44;
A5: InputVertices (1GateCircStr (<*x,y,z*>,f)) =
rng <*x,y,z*>
by CIRCCOMB:42
.=
{x,y,z}
by FINSEQ_2:128
;
then A6:
z in InputVertices (1GateCircStr (<*x,y,z*>,f))
by ENUMSET1:def 1;
( x in InputVertices (1GateCircStr (<*x,y,z*>,f)) & y in InputVertices (1GateCircStr (<*x,y,z*>,f)) )
by A5, ENUMSET1:def 1;
hence
( (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z )
by A6, CIRCUIT2:def 5; verum