let x, y, c be object ; :: thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
Following (s,2) is stable
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
Following (s,2) is stable
let s be State of (2GatesCircuit (x,y,c,f)); :: thesis: ( c <> [<*x,y*>,f] implies Following (s,2) is stable )
set S = 2GatesCircStr (x,y,c,f);
assume A1: c <> [<*x,y*>,f] ; :: thesis: Following (s,2) is stable

now :: thesis: ( dom (Following (Following (s,2))) = the carrier of (2GatesCircStr (x,y,c,f)) & dom (Following (s,2)) = the carrier of (2GatesCircStr (x,y,c,f)) & ( for a being object st a in the carrier of (2GatesCircStr (x,y,c,f)) holds
(Following (Following (s,2))) . a = (Following (s,2)) . a ) )

thus ( dom (Following (Following (s,2))) = the carrier of (2GatesCircStr (x,y,c,f)) & dom (Following (s,2)) = the carrier of (2GatesCircStr (x,y,c,f)) ) by CIRCUIT1:3; :: thesis: for a being object st a in the carrier of (2GatesCircStr (x,y,c,f)) holds
(Following (Following (s,2))) . b₂ = (Following (s,2)) . b₂
let a be object ; :: thesis: ( a in the carrier of (2GatesCircStr (x,y,c,f)) implies (Following (Following (s,2))) . b₁ = (Following (s,2)) . b₁ )
A2: (InputVertices (2GatesCircStr (x,y,c,f))) \/ (InnerVertices (2GatesCircStr (x,y,c,f))) = the carrier of (2GatesCircStr (x,y,c,f)) by XBOOLE_1:45;
assume a in the carrier of (2GatesCircStr (x,y,c,f)) ; :: thesis: (Following (Following (s,2))) . b₁ = (Following (s,2)) . b₁
then reconsider v = a as Vertex of (2GatesCircStr (x,y,c,f)) ;
A3: InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by Th56;
A4: (Following (s,2)) . c = s . c by A1, Th62;
A5: ( (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y ) by A1, Th62;
A6: ( (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . (2GatesCircOutput (x,y,c,f)) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> ) by A1, Th62;
A7: InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c} by A1, Th57;

per cases ( v in InputVertices (2GatesCircStr (x,y,c,f)) or v in InnerVertices (2GatesCircStr (x,y,c,f)) ) by A2, XBOOLE_0:def 3;

suppose v in InputVertices (2GatesCircStr (x,y,c,f)) ; :: thesis: (Following (Following (s,2))) . b₁ = (Following (s,2)) . b₁

then ( v = x or v = y or v = c ) by A7, ENUMSET1:def 1;
hence (Following (Following (s,2))) . a = (Following (s,2)) . a by A1, Lm1; :: thesis: verum

end;

suppose v in InnerVertices (2GatesCircStr (x,y,c,f)) ; :: thesis: (Following (Following (s,2))) . b₁ = (Following (s,2)) . b₁

then ( v = [<*x,y*>,f] or v = 2GatesCircOutput (x,y,c,f) ) by A3, TARSKI:def 2;
hence (Following (Following (s,2))) . a = (Following (s,2)) . a by A1, A6, A5, A4, Lm1; :: thesis: verum

end;

end;

end;

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