let S be non empty non void Circuit-like ManySortedSign ; for A being non-empty Circuit of S
for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following ((Following s),n)
let A be non-empty Circuit of S; for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following ((Following s),n)
let s be State of A; for n being Nat holds Following (s,(n + 1)) = Following ((Following s),n)
let n be Nat; Following (s,(n + 1)) = Following ((Following s),n)
Following (s,(n + 1)) = Following ((Following (s,1)),n)
by Th13;
hence
Following (s,(n + 1)) = Following ((Following s),n)
by Th14; verum