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)

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

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

A5:
rng (the_arity_of g) c= the carrier of S
by FINSEQ_1:def 4;((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;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

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