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)
( rng (the_arity_of g) c= the carrier of S & dom s = the carrier of S & dom (Following s,n) = the carrier of S ) by CIRCUIT1:4, FINSEQ_1:def 4;
then A2: ( dom ((Following s,n) * (the_arity_of g)) = dom (the_arity_of g) & dom (s * (the_arity_of g)) = dom (the_arity_of g) ) by RELAT_1:46;

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 a in dom (the_arity_of g) ; :: thesis: ((Following s,n) * (the_arity_of g)) . a = (s * (the_arity_of g)) . a
then A3: ( ((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) & (the_arity_of g) . a in rng (the_arity_of g) ) by FUNCT_1:23, FUNCT_1:def 5;
then s is_stable_at (the_arity_of g) . a by A1;
hence ((Following s,n) * (the_arity_of g)) . a = (s * (the_arity_of g)) . a by A3, Def9; :: thesis: verum

end;

then A4: (Following s,n) * (the_arity_of g) = s * (the_arity_of g) by 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 A4, Th10 ; :: thesis: verum