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 holds (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))

let A be non-empty Circuit of S; :: thesis: for s being State of A

for g being Gate of S holds (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))

let s be State of A; :: thesis: for g being Gate of S holds (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))

let g be Gate of S; :: thesis: (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))

set v = the_result_sort_of g;

dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;

then the ResultSort of S . g in rng the ResultSort of S by FUNCT_1:def 3;

then A1: the_result_sort_of g in InnerVertices S by MSUALG_1:def 2;

then ( g depends_on_in s = s * (the_arity_of g) & action_at (the_result_sort_of g) = g ) by CIRCUIT1:def 3, MSAFREE2:def 7;

hence (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g)) by A1, CIRCUIT2:def 5; :: thesis: verum

for s being State of A

for g being Gate of S holds (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))

let A be non-empty Circuit of S; :: thesis: for s being State of A

for g being Gate of S holds (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))

let s be State of A; :: thesis: for g being Gate of S holds (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))

let g be Gate of S; :: thesis: (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))

set v = the_result_sort_of g;

dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;

then the ResultSort of S . g in rng the ResultSort of S by FUNCT_1:def 3;

then A1: the_result_sort_of g in InnerVertices S by MSUALG_1:def 2;

then ( g depends_on_in s = s * (the_arity_of g) & action_at (the_result_sort_of g) = g ) by CIRCUIT1:def 3, MSAFREE2:def 7;

hence (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g)) by A1, CIRCUIT2:def 5; :: thesis: verum