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: ( dom (Following s) = the carrier of (BitCompStr x,b) & dom (Following (Following s)) = the carrier of (BitCompStr x,b) ) by CIRCUIT1:4;
A2: the carrier of (BitCompStr x,b) = {x,b} \/ {[<*x,b*>,xor2a ],[<*x,b*>,and2a ]} by Th48;

now

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

end;

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