:: deftheorem defines is_stable_at FACIRC_1:def 9 :
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 x being object holds
( s is_stable_at x iff for n being Nat holds (Following (s,n)) . x = s . x );