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 Th37;

A2: now :: thesis: for a being object st a in the carrier of (BitCompStr (x,b)) holds
(Following (Following s)) . a = (Following s) . a

let a be object ; :: 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 Th45 ;
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 Th49 ;
A6: (Following (Following s)) . [<*x,b*>,xor2a] = (Following (Following s)) . (CompOutput (x,b))
.= xor2a . <*((Following s) . x),((Following s) . b)*> by Th45 ;
A7: (Following s) . [<*x,b*>,and2a] = (Following s) . (IncrementOutput (x,b))
.= and2a . <*(s . x),(s . b)*> by Th49 ;
(Following s) . x = s . x by Th45;
hence (Following (Following s)) . a = (Following s) . a by A4, A3, A7, A6, A5, Th45; :: thesis: verum

end;

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