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 holds Following (s,0) = s

let A be non-empty Circuit of S; :: thesis: for s being State of A holds Following (s,0) = s

let s be State of A; :: thesis: Following (s,0) = s

ex f being sequence of (product the Sorts of A) st

( Following (s,0) = f . 0 & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) by Def7;

hence Following (s,0) = s ; :: thesis: verum

for s being State of A holds Following (s,0) = s

let A be non-empty Circuit of S; :: thesis: for s being State of A holds Following (s,0) = s

let s be State of A; :: thesis: Following (s,0) = s

ex f being sequence of (product the Sorts of A) st

( Following (s,0) = f . 0 & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) by Def7;

hence Following (s,0) = s ; :: thesis: verum