let x, b be non pair set ; :: thesis: for s being State of (BitCompCirc x,b) holds Following s is stable
set p = <*x,b*>;
set S = BitCompStr x,b;
let s be State of (BitCompCirc x,b); :: thesis: Following s is stable
set s1 = Following s;
set s2 = Following (Following s);
A1: the carrier of (BitCompStr x,b) = {x,b} \/ {[<*x,b*>,xor2a ],[<*x,b*>,and2a ]} by Th48;

A2: now

let a be set ; :: thesis: ( a in the carrier of (BitCompStr x,b) implies (Following (Following s)) . a = (Following s) . a )
A3: (Following s) . [<*x,b*>,xor2a ] = (Following s) . (CompOutput x,b)
.= xor2a . <*(s . x),(s . b)*> by Th56 ;
assume a in the carrier of (BitCompStr x,b) ; :: thesis: (Following (Following s)) . a = (Following s) . a
then ( a in {x,b} or a in {[<*x,b*>,xor2a ],[<*x,b*>,and2a ]} ) by A1, XBOOLE_0:def 3;
then A4: ( a = x or a = b or a = [<*x,b*>,xor2a ] or a = [<*x,b*>,and2a ] ) by TARSKI:def 2;
A5: (Following (Following s)) . [<*x,b*>,and2a ] = (Following (Following s)) . (IncrementOutput x,b)
.= and2a . <*((Following s) . x),((Following s) . b)*> by Th60 ;
A6: (Following (Following s)) . [<*x,b*>,xor2a ] = (Following (Following s)) . (CompOutput x,b)
.= xor2a . <*((Following s) . x),((Following s) . b)*> by Th56 ;
A7: (Following s) . [<*x,b*>,and2a ] = (Following s) . (IncrementOutput x,b)
.= and2a . <*(s . x),(s . b)*> by Th60 ;
(Following s) . x = s . x by Th56;
hence (Following (Following s)) . a = (Following s) . a by A4, A3, A7, A6, A5, Th56; :: thesis: verum

end;

( dom (Following s) = the carrier of (BitCompStr x,b) & dom (Following (Following s)) = the carrier of (BitCompStr x,b) ) by CIRCUIT1:4;
hence Following s = Following (Following s) by A2, FUNCT_1:9; :: according to CIRCUIT2:def 6 :: thesis: verum