theorem Th17: :: CIRCCOMB:17

for S1, S being non empty non void Circuit-like ManySortedSign
for S2 being non empty ManySortedSign st S1 tolerates S2 & S = S1 +* S2 holds
for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v being Vertex of S st v1 = v holds
( v in InnerVertices S & action_at v = action_at v1 )