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