theorem Th32: :: FACIRC_1:32

for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S2 misses InputVertices S1 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for v being set st v in the carrier of S1 holds
for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v