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