let x, b be non pair set ; for s being State of (IncrementCirc (x,b)) holds
( (Following s) . (IncrementOutput (x,b)) = and2a . <*(s . x),(s . b)*> & (Following s) . x = s . x & (Following s) . b = s . b )
let s be State of (IncrementCirc (x,b)); ( (Following s) . (IncrementOutput (x,b)) = and2a . <*(s . x),(s . b)*> & (Following s) . x = s . x & (Following s) . b = s . b )
set p = <*x,b*>;
set S = IncrementStr (x,b);
A1:
( dom s = the carrier of (IncrementStr (x,b)) & x in the carrier of (IncrementStr (x,b)) )
by CIRCUIT1:3, FACIRC_1:43;
A2:
b in the carrier of (IncrementStr (x,b))
by FACIRC_1:43;
InnerVertices (IncrementStr (x,b)) = the carrier' of (IncrementStr (x,b))
by FACIRC_1:37;
hence (Following s) . (IncrementOutput (x,b)) =
and2a . (s * <*x,b*>)
by FACIRC_1:35
.=
and2a . <*(s . x),(s . b)*>
by A1, A2, FINSEQ_2:125
;
( (Following s) . x = s . x & (Following s) . b = s . b )
InputVertices (IncrementStr (x,b)) = {x,b}
by FACIRC_1:40;
then
( x in InputVertices (IncrementStr (x,b)) & b in InputVertices (IncrementStr (x,b)) )
by TARSKI:def 2;
hence
( (Following s) . x = s . x & (Following s) . b = s . b )
by CIRCUIT2:def 5; verum