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 x being set st s is_stable_at x holds

for n being Nat holds Following (s,n) is_stable_at x

let A be non-empty Circuit of S; :: thesis: for s being State of A

for x being set st s is_stable_at x holds

for n being Nat holds Following (s,n) is_stable_at x

let s be State of A; :: thesis: for x being set st s is_stable_at x holds

for n being Nat holds Following (s,n) is_stable_at x

let x be set ; :: thesis: ( s is_stable_at x implies for n being Nat holds Following (s,n) is_stable_at x )

assume A1: for n being Nat holds (Following (s,n)) . x = s . x ; :: according to FACIRC_1:def 9 :: thesis: for n being Nat holds Following (s,n) is_stable_at x

let n, m be Nat; :: according to FACIRC_1:def 9 :: thesis: (Following ((Following (s,n)),m)) . x = (Following (s,n)) . x

thus (Following ((Following (s,n)),m)) . x = (Following (s,(n + m))) . x by Th13

.= s . x by A1

.= (Following (s,n)) . x by A1 ; :: thesis: verum

for s being State of A

for x being set st s is_stable_at x holds

for n being Nat holds Following (s,n) is_stable_at x

let A be non-empty Circuit of S; :: thesis: for s being State of A

for x being set st s is_stable_at x holds

for n being Nat holds Following (s,n) is_stable_at x

let s be State of A; :: thesis: for x being set st s is_stable_at x holds

for n being Nat holds Following (s,n) is_stable_at x

let x be set ; :: thesis: ( s is_stable_at x implies for n being Nat holds Following (s,n) is_stable_at x )

assume A1: for n being Nat holds (Following (s,n)) . x = s . x ; :: according to FACIRC_1:def 9 :: thesis: for n being Nat holds Following (s,n) is_stable_at x

let n, m be Nat; :: according to FACIRC_1:def 9 :: thesis: (Following ((Following (s,n)),m)) . x = (Following (s,n)) . x

thus (Following ((Following (s,n)),m)) . x = (Following (s,(n + m))) . x by Th13

.= s . x by A1

.= (Following (s,n)) . x by A1 ; :: thesis: verum