let S be non empty non void Circuit-like ManySortedSign ; :: thesis: for A being non-empty Circuit of S
for s being State of A
for x being set st x in InputVertices S holds
s is_stable_at x
let A be non-empty Circuit of S; :: thesis: for s being State of A
for x being set st x in InputVertices S holds
s is_stable_at x
let s be State of A; :: thesis: for x being set st x in InputVertices S holds
s is_stable_at x
let x be set ; :: thesis: ( x in InputVertices S implies s is_stable_at x )
defpred S₁[ Nat] means (Following (s,$1)) . x = s . x;
assume A1: x in InputVertices S ; :: thesis: s is_stable_at x

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
(Following (s,(n + 1))) . x = (Following (Following (s,n))) . x by Th12
.= s . x by A1, A3, CIRCUIT2:def 5 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A4: S₁[ 0 ] by Th11;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A2); :: according to FACIRC_1:def 9 :: thesis: verum