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 st s is stable holds
for n being Nat holds Following (s,n) = s
let A be non-empty Circuit of S; :: thesis: for s being State of A st s is stable holds
for n being Nat holds Following (s,n) = s
let s be State of A; :: thesis: ( s is stable implies for n being Nat holds Following (s,n) = s )
assume A1: s is stable ; :: thesis: for n being Nat holds Following (s,n) = s
defpred S₁[ Nat] means Following (s,$1) = s;

A2: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then Following (Following (s,n)) = s by A1, CIRCUIT2:def 6;
hence S₁[n + 1] by FACIRC_1:12; :: thesis: verum

end;

A3: S₁[ 0 ] by FACIRC_1:11;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A2); :: thesis: verum