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 is stable
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 is stable
let f be Function of (3 -tuples_on X),X; :: thesis: for s being State of (1GateCircuit <*x,y,z*>,f) holds Following s is stable
set p = <*x,y,z*>;
set S = 1GateCircStr <*x,y,z*>,f;
let s be State of (1GateCircuit <*x,y,z*>,f); :: thesis: Following s is stable
set s1 = Following s;
set s2 = Following (Following s);
A1: ( dom (Following s) = the carrier of (1GateCircStr <*x,y,z*>,f) & dom (Following (Following s)) = the carrier of (1GateCircStr <*x,y,z*>,f) ) by CIRCUIT1:4;
A2: the carrier of (1GateCircStr <*x,y,z*>,f) = (rng <*x,y,z*>) \/ {[<*x,y,z*>,f]} by CIRCCOMB:def 6
.= {x,y,z} \/ {[<*x,y,z*>,f]} by FINSEQ_2:148 ;

now

let a be set ; :: thesis: ( a in the carrier of (1GateCircStr <*x,y,z*>,f) implies (Following (Following s)) . a = (Following s) . a )
assume a in the carrier of (1GateCircStr <*x,y,z*>,f) ; :: thesis: (Following (Following s)) . a = (Following s) . a
then ( a in {x,y,z} or a in {[<*x,y,z*>,f]} ) by A2, XBOOLE_0:def 3;
then A3: ( a = x or a = y or a = z or a = [<*x,y,z*>,f] ) by ENUMSET1:def 1, TARSKI:def 1;
( (Following (Following s)) . x = (Following s) . x & (Following s) . x = s . x & (Following (Following s)) . y = (Following s) . y & (Following s) . y = s . y & (Following (Following s)) . z = (Following s) . z & (Following s) . z = s . z & (Following (Following s)) . [<*x,y,z*>,f] = f . <*((Following s) . x),((Following s) . y),((Following s) . z)*> & (Following s) . [<*x,y,z*>,f] = f . <*(s . x),(s . y),(s . z)*> ) by Th52;
hence (Following (Following s)) . a = (Following s) . a by A3; :: thesis: verum

end;

hence Following s = Following (Following s) by A1, FUNCT_1:9; :: according to CIRCUIT2:def 6 :: thesis: verum