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 :: thesis: for a being object st a in dom (the_arity_of g) holds
((Following (s,n)) * (the_arity_of g)) . a = (s * (the_arity_of g)) . a

let a be object ; :: 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 3;
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:13;
hence ((Following (s,n)) * (the_arity_of g)) . a = (s * (the_arity_of g)) . a by A4; :: 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:3;
then A6: dom ((Following (s,n)) * (the_arity_of g)) = dom (the_arity_of g) by A5, RELAT_1:27;
dom s = the carrier of S by CIRCUIT1:3;
then dom (s * (the_arity_of g)) = dom (the_arity_of g) by A5, RELAT_1:27;
then A7: (Following (s,n)) * (the_arity_of g) = s * (the_arity_of g) by A6, A2, FUNCT_1:2;
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