:: deftheorem Def7 defines Following FACIRC_1:def 8 :
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n being natural Number
for b₅ being State of A holds
( b₅ = Following (s,n) iff ex f being sequence of (product the Sorts of A) st
( b₅ = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) );