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 n being Nat holds Following (s,(n + 1)) = Following ((Following s),n)

let A be non-empty Circuit of S; :: thesis: 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; :: thesis: for n being Nat holds Following (s,(n + 1)) = Following ((Following s),n)

let n be Nat; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: for n being Nat holds Following (s,(n + 1)) = Following ((Following s),n)

let n be Nat; :: thesis: 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; :: thesis: verum