let x, y, z be set ; :: 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*>;
( x in {x,y,z} & y in {x,y,z} & z in {x,y,z} & dom s = the carrier of (1GateCircStr <*x,y,z*>,f) ) by CIRCUIT1:4, ENUMSET1:def 1;
then ( x in rng <*x,y,z*> & y in rng <*x,y,z*> & z in rng <*x,y,z*> & dom s = (rng <*x,y,z*>) \/ {[<*x,y,z*>,f]} ) by CIRCCOMB:def 6, FINSEQ_2:148;
then A1: ( x in dom s & y in dom s & z in dom s ) by XBOOLE_0:def 3;
thus (Following s) . [<*x,y,z*>,f] = f . (s * <*x,y,z*>) by CIRCCOMB:64
.= f . <*(s . x),(s . y),(s . z)*> by A1, FINSEQ_2:146 ; :: 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;
InputVertices (1GateCircStr <*x,y,z*>,f) = rng <*x,y,z*> by CIRCCOMB:49
.= {x,y,z} by FINSEQ_2:148 ;
then ( x in InputVertices (1GateCircStr <*x,y,z*>,f) & y in InputVertices (1GateCircStr <*x,y,z*>,f) & z in InputVertices (1GateCircStr <*x,y,z*>,f) ) by ENUMSET1:def 1;
hence ( (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z ) by CIRCUIT2:def 5; :: thesis: verum