theorem Th7: :: FACIRC_1:7

for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st InputVertices S1 is without_pairs & InnerVertices S1 is Relation & InputVertices S2 is without_pairs & InnerVertices S2 is Relation holds
InputVertices (S1 +* S2) = (InputVertices S1) \/ (InputVertices S2)