let S be non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; :: thesis: for A being non-empty gate`2=den Boolean Circuit of S
for s being State of A
for p being FinSequence
for f being Function st [p,f] in the carrier' of S holds
(Following s) . [p,f] = f . (s * p)
let A be non-empty gate`2=den Boolean Circuit of S; :: thesis: for s being State of A
for p being FinSequence
for f being Function st [p,f] in the carrier' of S holds
(Following s) . [p,f] = f . (s * p)
let s be State of A; :: thesis: for p being FinSequence
for f being Function st [p,f] in the carrier' of S holds
(Following s) . [p,f] = f . (s * p)
let p be FinSequence; :: thesis: for f being Function st [p,f] in the carrier' of S holds
(Following s) . [p,f] = f . (s * p)
let f be Function; :: thesis: ( [p,f] in the carrier' of S implies (Following s) . [p,f] = f . (s * p) )
assume [p,f] in the carrier' of S ; :: thesis: (Following s) . [p,f] = f . (s * p)
then reconsider g = [p,f] as Gate of S ;
A2: the_arity_of g = the Arity of S . g by MSUALG_1:def 6
.= [(the Arity of S . g),(g `2 )] `1 by MCART_1:7
.= g `1 by CIRCCOMB:def 8 ;
A3: ( g `1 = p & g `2 = f ) by MCART_1:7;
the_result_sort_of g = the ResultSort of S . g by MSUALG_1:def 7
.= g by CIRCCOMB:52 ;
hence (Following s) . [p,f] = f . (s * p) by A2, A3, Th34; :: thesis: verum