let S be non empty non void Circuit-like gate`2=den ManySortedSign ; :: thesis: for A being non-empty Circuit of S st A is gate`2=den holds
for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (g `2) . (s * (the_arity_of g))
let A be non-empty Circuit of S; :: thesis: ( A is gate`2=den implies for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (g `2) . (s * (the_arity_of g)) )
assume A1: for g being set st g in the carrier' of S holds
g = [(g `1),( the Charact of A . g)] ; :: according to CIRCCOMB:def 10 :: thesis: for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (g `2) . (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) = (g `2) . (s * (the_arity_of g))
let g be Gate of S; :: thesis: (Following s) . (the_result_sort_of g) = (g `2) . (s * (the_arity_of g))
A2: Den (g,A) = the Charact of A . g by MSUALG_1:def 6
.= [(g `1),( the Charact of A . g)] `2
.= g `2 by A1 ;
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 A3: 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) = (g `2) . (s * (the_arity_of g)) by A2, A3, CIRCUIT2:def 5; :: thesis: verum