let X be non empty finite set ; :: thesis: for n being Nat
for p being FinSeqLen of n
for f being Function of n -tuples_on X,X
for s being State of (1GateCircuit p,f) holds Following s is stable
let n be Nat; :: thesis: for p being FinSeqLen of n
for f being Function of n -tuples_on X,X
for s being State of (1GateCircuit p,f) holds Following s is stable
let p be FinSeqLen of n; :: thesis: for f being Function of n -tuples_on X,X
for s being State of (1GateCircuit p,f) holds Following s is stable
let f be Function of n -tuples_on X,X; :: thesis: for s being State of (1GateCircuit p,f) holds Following s is stable
set S = 1GateCircStr p,f;
let s be State of (1GateCircuit p,f); :: thesis: Following s is stable
set s1 = Following s;
set s2 = Following (Following s);
A1: ( dom (Following s) = the carrier of (1GateCircStr p,f) & dom (Following (Following s)) = the carrier of (1GateCircStr p,f) ) by CIRCUIT1:4;
A2: the carrier of (1GateCircStr p,f) = (rng p) \/ {[p,f]} by CIRCCOMB:def 6;
A3: ( InputVertices (1GateCircStr p,f) = rng p & InnerVertices (1GateCircStr p,f) = {[p,f]} ) by CIRCCOMB:49;

now

let a be set ; :: thesis: ( a in the carrier of (1GateCircStr p,f) implies (Following (Following s)) . a = (Following s) . a )
assume a in the carrier of (1GateCircStr p,f) ; :: thesis: (Following (Following s)) . a = (Following s) . a
then reconsider v = a as Vertex of (1GateCircStr p,f) ;
A4: (Following s) * p = s * p

proof

dom s = the carrier of (1GateCircStr p,f) by CIRCUIT1:4;
then A5: ( dom ((Following s) * p) = dom p & dom (s * p) = dom p ) by A1, A2, RELAT_1:46, XBOOLE_1:7;

now

let i be set ; :: thesis: ( i in dom p implies ((Following s) * p) . i = (s * p) . i )
assume A6: i in dom p ; :: thesis: ((Following s) * p) . i = (s * p) . i
then A7: ( ((Following s) * p) . i = (Following s) . (p . i) & (s * p) . i = s . (p . i) ) by A5, FUNCT_1:22;
p . i in rng p by A6, FUNCT_1:12;
hence ((Following s) * p) . i = (s * p) . i by A3, A7, CIRCUIT2:def 5; :: thesis: verum

end;

hence (Following s) * p = s * p by A5, FUNCT_1:9; :: thesis: verum

end;

( v in rng p or v in {[p,f]} ) by A2, XBOOLE_0:def 3;
then ( (Following (Following s)) . v = (Following s) . v or ( v = [p,f] & ( v = [p,f] implies action_at v = v ) & (Following (Following s)) . v = (Den (action_at v),(1GateCircuit p,f)) . ((action_at v) depends_on_in (Following s)) & (Following s) . v = (Den (action_at v),(1GateCircuit p,f)) . ((action_at v) depends_on_in s) & ( action_at v = [p,f] implies ( (action_at v) depends_on_in s = s * p & (action_at v) depends_on_in (Following s) = (Following s) * p ) ) ) ) by A3, Th1, CIRCCOMB:48, CIRCUIT2:def 5, TARSKI:def 1;
hence (Following (Following s)) . a = (Following s) . a by A4; :: thesis: verum

end;

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