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