let X be non empty finite set ; :: thesis: for n being Nat
for p being FinSeqLen of n
for f being Function of (),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 (),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 (),X
for s being State of (1GateCircuit (p,f)) holds Following s is stable

let f be Function of (),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:
set s1 = Following s;
set s2 = Following ();
A1: dom () = the carrier of (1GateCircStr (p,f)) by CIRCUIT1:3;
A2: the carrier of (1GateCircStr (p,f)) = (rng p) \/ {[p,f]} by CIRCCOMB:def 6;
A3: InputVertices (1GateCircStr (p,f)) = rng p by CIRCCOMB:42;
A4: InnerVertices (1GateCircStr (p,f)) = {[p,f]} by CIRCCOMB:42;
A5: now :: thesis: for a being object st a in the carrier of (1GateCircStr (p,f)) holds
() . a = () . a
let a be object ; :: thesis: ( a in the carrier of (1GateCircStr (p,f)) implies () . a = () . a )
assume a in the carrier of (1GateCircStr (p,f)) ; :: thesis: () . a = () . a
then reconsider v = a as Vertex of (1GateCircStr (p,f)) ;
dom s = the carrier of (1GateCircStr (p,f)) by CIRCUIT1:3;
then A6: dom (s * p) = dom p by ;
A7: dom (() * p) = dom p by ;
A8: now :: thesis: for i being object st i in dom p holds
(() * p) . i = (s * p) . i
let i be object ; :: thesis: ( i in dom p implies (() * p) . i = (s * p) . i )
assume A9: i in dom p ; :: thesis: (() * p) . i = (s * p) . i
then A10: p . i in rng p by FUNCT_1:3;
( ((Following s) * p) . i = () . (p . i) & (s * p) . i = s . (p . i) ) by ;
hence ((Following s) * p) . i = (s * p) . i by ; :: thesis: verum
end;
( v in rng p or v in {[p,f]} ) by ;
then ( (Following ()) . v = () . v or ( v = [p,f] & ( v = [p,f] implies action_at v = v ) & () . v = (Den ((),(1GateCircuit (p,f)))) . (() depends_on_in ()) & () . v = (Den ((),(1GateCircuit (p,f)))) . () & ( action_at v = [p,f] implies ( () depends_on_in s = s * p & () depends_on_in () = () * p ) ) ) ) by ;
hence (Following ()) . a = () . a by ; :: thesis: verum
end;
dom () = the carrier of (1GateCircStr (p,f)) by CIRCUIT1:3;
hence Following s = Following () by ; :: according to CIRCUIT2:def 6 :: thesis: verum