theorem Th29: :: FACIRC_1:29

for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S1 misses InputVertices S2 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 s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2