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

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