let x, y, z be object ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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)); :: thesis: ( (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 ; :: thesis: ( (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; :: thesis: verum

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 ; :: thesis: 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; :: thesis: 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)); :: thesis: ( (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 ; :: thesis: ( (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; :: thesis: verum