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 g being Gate of S st ( for x being set st x in rng (the_arity_of g) holds
s is_stable_at x ) holds
Following s is_stable_at the_result_sort_of g
let A be non-empty Circuit of S; :: thesis: for s being State of A
for g being Gate of S st ( for x being set st x in rng (the_arity_of g) holds
s is_stable_at x ) holds
Following s is_stable_at the_result_sort_of g
let s be State of A; :: thesis: for g being Gate of S st ( for x being set st x in rng (the_arity_of g) holds
s is_stable_at x ) holds
Following s is_stable_at the_result_sort_of g
let g be Gate of S; :: thesis: ( ( for x being set st x in rng (the_arity_of g) holds
s is_stable_at x ) implies Following s is_stable_at the_result_sort_of g )
set p = the_arity_of g;
assume A1: for x being set st x in rng (the_arity_of g) holds
s is_stable_at x ; :: thesis: Following s is_stable_at the_result_sort_of g
let n be Nat; :: according to FACIRC_1:def 9 :: thesis: (Following (Following s),n) . (the_result_sort_of g) = (Following s) . (the_result_sort_of g)

A2: now

let a be set ; :: thesis: ( a in dom (the_arity_of g) implies ((Following s,n) * (the_arity_of g)) . a = (s * (the_arity_of g)) . a )
assume A3: a in dom (the_arity_of g) ; :: thesis: ((Following s,n) * (the_arity_of g)) . a = (s * (the_arity_of g)) . a
then (the_arity_of g) . a in rng (the_arity_of g) by FUNCT_1:def 5;
then A4: s is_stable_at (the_arity_of g) . a by A1;
( ((Following s,n) * (the_arity_of g)) . a = (Following s,n) . ((the_arity_of g) . a) & (s * (the_arity_of g)) . a = s . ((the_arity_of g) . a) ) by A3, FUNCT_1:23;
hence ((Following s,n) * (the_arity_of g)) . a = (s * (the_arity_of g)) . a by A4, Def9; :: thesis: verum

end;

A5: rng (the_arity_of g) c= the carrier of S by FINSEQ_1:def 4;
dom (Following s,n) = the carrier of S by CIRCUIT1:4;
then A6: dom ((Following s,n) * (the_arity_of g)) = dom (the_arity_of g) by A5, RELAT_1:46;
dom s = the carrier of S by CIRCUIT1:4;
then dom (s * (the_arity_of g)) = dom (the_arity_of g) by A5, RELAT_1:46;
then A7: (Following s,n) * (the_arity_of g) = s * (the_arity_of g) by A6, A2, FUNCT_1:9;
thus (Following (Following s),n) . (the_result_sort_of g) = (Following s,(n + 1)) . (the_result_sort_of g) by Th16
.= (Following (Following s,n)) . (the_result_sort_of g) by Th12
.= (Den g,A) . ((Following s,n) * (the_arity_of g)) by Th10
.= (Following s) . (the_result_sort_of g) by A7, Th10 ; :: thesis: verum